Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 4/2014

01.08.2014 | TASE 12

Formal verification and simulation for platform screen doors and collision avoidance in subway control systems

verfasst von: Huixing Fang, Jianqi Shi, Huibiao Zhu, Jian Guo, Kim Guldstrand Larsen, Alexandre David

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 4/2014

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

For hybrid systems, hybrid automata-based tools are capable of verification, while Matlab Simulink/Stateflow is proficient in simulation. We propose a co-verification procedure, in which the verification tool SpaceEx/PHAVer and simulation tool Matlab are integrated to analyze and verify hybrid systems. For the application of this procedure, a platform screen door system (PSDS, a subsystem of the subway control system), is modeled with hybrid automata and Simulink/Stateflow charts, respectively. The models of PSDS are simulated by Matlab and verified by SpaceEx/PHAVer. The simulation and verification results indicate that the sandwiched situation can be avoided under time interval conditions. We improve the model with four trains and four stations on a subway line and analyze the urgent control scenario for the safety distance requirement. In this paper, the Simulink/Stateflow model is a refinement of the SpaceEx/PHAVer model, which is closer to a final implementation. Moreover, the two models are complementary for some features (e.g.,visualization of simulation, correctness proving by verification), stressing different aspects of the overall system and permitting complementary analysis techniques, i.e., verification versus simulation. We conclude that this integration procedure is competent in verifying subway control systems.
Vorheriger Artikel Program verification and testing technologies
Nächster Artikel Expressive program verification via structured specifications

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
Literatur
1.
Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
2.
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRef
3.
Abrial, J.-R., Lee, M., Neilson, D., Scharbach, P., SÃrensen, I.: The b-method. In: Proceedings of VDM, LNCS, vol. 552, pp. 398–405. Springer-Verlag, Berlin (1991)
4.
5.
Agrawal, A., Simon, G., Karsai, G.: Semantic translation of simulink/stateflow models to hybrid automata using graph transformations. Electron. Notes. Theor. Comput. Sci. 109, 43–56 (2004)CrossRef
6.
Alur, R., Courcoubetis, C., Henzinger, T., Ho, P.: Hybrid automata: an algorithmic approach to the specification and analysis of hybrid systems. In: Hybrid Systems, LNCS, vol. 736, pp. 209–229. Springer-Verlag, Berlin (1993)
7.
Alur, R., Henzinger, T., Ho, P.: Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22(3), 181–201 (1996)CrossRef
8.
Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Proceedings of HSCC, LNCS, vol. 1790, pp. 20–31. Springer-Verlag, Berlin (2000)
9.
Asarin, E., Dang, T., Maler, O., Testylier, R.: Using redundant constraints for refinement. In: Proceedings of ATVA, LNCS, vol. 6252, pp. 37–51. Springer-Verlag, Berlin (2010)
10.
Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Proceedings of SAS, LNCS, vol. 2477, pp. 299–315. Springer-Verlag, Berlin (2002)
11.
Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., Könighofer, R., Roveri, M., Schuppan, V., Seeber, R.: Ratsy-a new requirements analysis tool with synthesis. In: Proceedings of CAV, pp. 425–429. Springer-Verlag, Berlin (2010)
12.
Bonnett, C.: Practical Railway Engineering. Imperial College Press, London (2005)CrossRef
13.
14.
15.
16.
Doyen, L., Henzinger, T., Raskin, J.: Automatic rectangular refinement of affine hybrid systems. In: Proceedings of FORMATS, LNCS, vol. 3829, pp. 144–161. Springer-Verlag, Berlin (2005)
17.
Ferrari, A., Fantechi, A., Magnani, G., Grasso, D., Tempestini, M.: The metrô rio case study. Sci. Comput. Program. 78(7), 828–842 (2012)CrossRef
18.
Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Proceedings of HSCC, LNCS, vol. 3414, pp. 258–273. Springer-Verlag, Berlin (2005)
19.
20.
Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools. Technol. Transf. 10(3), 263–279 (2008)CrossRefMathSciNet
21.
Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Proceedings of CAV, LNCS, vol. 6806, pp. 379–395. Springer-Verlag, Berlin (2011)
22.
Girard, A., Le Guernic, C.: Zonotope/hyperplane intersection for hybrid systems reachability analysis. In: Proceedings of HSCC, LNCS, vol. 4981, pp. 215–228. Springer-Verlag, Berlin (2008)
23.
Granlund, T., Ryde, K.: The GNU Multiple Precision Arithmetic Library Version 4 (2001)
24.
Halbwachs, N., Proy, Y., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: Proceedings of SAS, LNCS, vol. 864, pp. 223–237. Springer-Verlag, Berlin (1994)
25.
Hamon, G.: A denotational semantics for stateflow. In: Proceedings of EMSOFT, pp. 164–172. ACM, New York (2005)
26.
Hamon, G., Rushby, J.: An operational semantics for stateflow. Int. J. Softw. Tools. Technol. Transf. 9(5–6), 447–456 (2007)CrossRef
27.
28.
Harel, D., Naamad, A.: The statemate semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293–333 (1996)CrossRef
29.
Henzinger, T., Ho, P., Wong-Toi, H.: Hytech: a model checker for hybrid systems. Int. J. Softw. Tools. Technol. Transf. 1(1–2), 110–122 (1997)CrossRefMATH
30.
Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)CrossRefMATHMathSciNet
31.
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of LICS, pp. 278–292. IEEE Computer Society, Washington, D.C. (1996)
32.
Jacky, J.: The Way of Z: Practical Programming with Formal Methods. Cambridge University Press, Cambridge (1996)CrossRef
33.
34.
Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Proceedings of HSCC, LNCS, vol. 1790, pp. 202–214. Springer-Verlag, Berlin (2000)
35.
Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250–262 (2010)CrossRefMATHMathSciNet
36.
Lecomte, T.: Safe and reliable metro platform screen doors control/command systems. In: Proceedings of FM, LNCS, vol. 5014, pp. 430–434. Springer-Verlag, Berlin (2008)
37.
Lecomte, T.: Applying a formal method in industry: a 15-year trajectory. In: Proceedings of FMICS, LNCS, vol. 5825, pp. 26–34. Springer-Verlag, Berlin (2009)
38.
Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations, ii: timing-based systems. Inf. Comput. 128(1), 1–25 (1996)CrossRefMATHMathSciNet
39.
Marrone, S., Nardone, R., Orazzo, A., Petrone, I., Velardi, L.: Improving verification process in driverless metro systems: the mbat project. In: Proceedings of ISoLA, LNCS, vol. 7610, pp. 231–245. Springer-Verlag, Berlin (2012)
40.
41.
42.
Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: An approach to the description and analysis of hybrid systems. In: Proceedings of Hybrid Systems, LNCS, vol. 736, pp. 149–178. Springer-Verlag, Berlin (1993)
43.
Ober, I., Graf, S., Ober, I.: Validating timed uml models by simulation and verification. Int. J. Softw. Tools. Technol. Transf. 8(2), 128–145 (2006)CrossRef
44.
Pinto, A., Sangiovanni-Vincentelli, A.L., Carloni, L.P., Passerone, R.: Interchange formats for hybrid systems: review and proposal. Proc. HSCC LNCS 3414, 526–541 (2005)
45.
Qu, L., Chow, W.: Platform screen doors on emergency evacuation in underground railway stations. Tunn. Undergr. Space Technol. 30, 1–9 (2012)CrossRef
46.
Roh, J.S., Ryou, H.S., Park, W.H., Jang, Y.J.: Cfd simulation and assessment of life safety in a subway train fire. Tunn. Undergr. Space Technol. 24(4), 447–453 (2009)CrossRef
47.
Su, W., Abrial, J.-R., Zhu, H.: Complementary methodologies for developing hybrid systems with event-b. In: Proceedings of ICFEM, LNCS, vol. 7635. Springer-Verlag, Berlin (2012)
48.
Zhao, L., Tang, T., Cheng, R., He, L.: Property based requirements analysis for train control system. J. Comput. Inf. Syst. 9(3), 915–922 (2013)
Metadaten
Titel
Formal verification and simulation for platform screen doors and collision avoidance in subway control systems
verfasst von
Huixing Fang
Jianqi Shi
Huibiao Zhu
Jian Guo
Kim Guldstrand Larsen
Alexandre David
Publikationsdatum
01.08.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 4/2014
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-014-0318-1

Weitere Artikel der Ausgabe 4/2014

International Journal on Software Tools for Technology Transfer 4/2014 Zur Ausgabe

Tase 12

Automated verification of the FreeRTOS scheduler in Hip/Sleek

TASE 12

Expressive program verification via structured specifications

Introduction

Program verification and testing technologies

TASE 12

Quantitative modelling and analysis of a Chinese smart grid: a stochastic model checking case study

TASE 12

Quantitative and qualitative analysis of SysML activity diagrams

TASE 12

Model-based test generation using extended symbolic grammars