nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

04.08.2015 | ABZ 2014

Rigorous development process of a safety-critical system: from ASM models to Java code

verfasst von: Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2017

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

The paper presents an approach for rigorous development of safety-critical systems based on the Abstract State Machine formal method. The development process starts from a high level formal view of the system and, through refinement, derives more detailed models till the desired level of specification. Along the process, different validation and verification activities are available, as simulation, model review, and model checking. Moreover, each refinement step can be proved correct using an SMT-based approach. As last step of the refinement process, a Java implementation can be developed and linked to the formal specification. The correctness of the implementation w.r.t. its formal specification can be proved by means of model-based testing and runtime verification. The process is exemplified by using a Landing Gear System as case study.

Vorheriger Artikel Environment-driven reachability for timed systems

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

http://asmeta.sourceforge.net/download/asmrefprover.html.

http://asmeta.sourceforge.net/.

Note that sequences generated by ATGT could be used to test programs written in any programming language.

All the models are available online at http://fmse.di.unimi.it/sw/LGS_STTT.zip.

In the case study [14], this behavior is described as follows: if the control software does not see the value \(door\_closed[x] = false\) for all \(x \in \{front, left, right\}\) 7 seconds after stimulation of the opening electro-valve, then the doors are considered as blocked and an anomaly is detected.

Pure methods are side effect free methods with respect to the object/program state. They return a value but do not assign values to fields.

We do not consider the default constructor. If the class does not have any constructor, the user has to specify an empty constructor and annotate it with @StartMonitoring.

The user can identify several changing methods, but, in this case, each changing method must be linked with a different monitored value by the two annotation attributes setFunction, specifying the name of a 0-ary monitored function of the ASM model, and toValue, specifying a value of the function codomain: setFunction must identify the same function in all the annotations, while toValue must assume different values.

Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York, NY, USA (2010)CrossRefMATH

Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Proceedings of the 2nd International Conference on Abstract State Machines, Alloy, B and Z (ABZ 2010), volume 5977 of Lecture Notes in Computer Science, pages 61–74. Springer (2010)

Arcaini, P., Gargantini, A., Riccobene, E.: Automatic Review of Abstract State Machines by Meta-Property Verification. In: Muñoz, C. (ed.) Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215, pp. 4–13. NASA (2010)

Arcaini, P., Gargantini, A., Riccobene, E.: CoMA: Conformance monitoring of Java programs by Abstract State Machines. In: Khurshid, S., Sen, K. (eds.) Runtime Verification volume 7186 of Lecture Notes in Computer Science, pp. 223–238. Springer (2012)

Arcaini, P., Gargantini, A., Riccobene, E.: Combining model-based testing and runtime monitoring for program testing in the presence of nondeterminism. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, Workshops Proceedings, Luxembourg, March 18-22, 2013, pp. 178–187. IEEE (2013)

Arcaini, P., Gargantini, A., Riccobene, E.: Modeling and Analyzing Using ASMs: The Landing Gear System Case Study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study volume 433 of Communications in Computer and Information Science, pp. 36–51. Springer International Publishing (2014)

Arcaini, P., Gargantini, A., Riccobene, E.: Offline Model-Based Testing and Runtime Monitoring of the Sensor Voting Module. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study volume 433 of Communications in Computer and Information Science, pp. 95–109. Springer International Publishing (2014)

Arcaini, P., Gargantini, A., Riccobene, E.: Using SMT for dealing with nondeterminism in ASM-based runtime verification. ECEASST 70 (2014)

Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw.: Pract. Exp. 41, 155–166 (2011)

10.

Banach, R.: The Landing Gear Case Study in Hybrid Event-B. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study volume 433 of Communications in Computer and Information Science, pp. 126–141. Springer International Publishing (2014)

11.

Barnett, M., Schulte, W.: Runtime verification of NET contracts. J. Syst. Softw. 65(3), 199–208 (2003)CrossRef

12.

Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Method. (TOSEM) 20 (2011)

13.

Berthomieu, B., Dal Zilio, S., Fronc, Ł.: Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 110–125. Springer International Publishing (2014)

14.

Boniol, F., Wiels, V.: The Landing Gear System Case Study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 1–18. Springer International Publishing (2014)

15.

Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K.-D.: ABZ 2014: The Landing Gear Case Study Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z Toulouse, France, June 2-6, 2014, Proceedings. Springer International Publishing (2014)

16.

Börger, E.: The ASM refinement method. Form. Aspects Comput. 15, 237–257 (2003)CrossRefMATH

17.

Börger, E.: The ASM method for system design and analysis. A tutorial introduction. In: Gramlich, B. (ed.) Proceedings of Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, volume 3717 of Lecture Notes in Computer Science, pp. 264–283. Springer (2005)

18.

Börger, E.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Berlin Heidelberg (2003)CrossRefMATH

19.

Carioni, A., Gargantini, A., Riccobene, E., Scandurra, P.: A Scenario-Based Validation Language for ASMs. In: Proceedings of the 1st International Conference on Abstract State Machines, B and Z (ABZ 2008), volume 5238 of Lecture Notes in Computer Science, pp. 71–84. Springer-Verlag (2008)

20.

Chen, F., D’Amorim, M., Roşu, G.: A formal monitoring-based framework for software development and analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) Formal Methods and Software Engineering, volume of 3308 LNCS, pp. 357–372. Springer, Berlin / Heidelberg (2004)

21.

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge, MA, USA (1999)

22.

Dausend, M., Raschke, A.: Introducing Aspect-Oriented Specification for Abstract State Machines. In: Ait Ameur, Y., Schewe, K.-D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, volume 8477 of Lecture Notes in Computer Science, pp. 174–187. Springer Berlin Heidelberg (2014)

23.

Dausend, M., Stegmaier, M., Raschke, A.: Debugging Abstract State Machine Specifications: An Extension of CoreASM. In: Mazzanti, F., Trentanni, G. (eds.) Proceedings of iFM 2012 & ABZ 2012 - Posters & Tool demos Session, pp. 21–25 (2012)

24.

Delgado, N., Gates, A.Q., Roach, S.: A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans. Softw. Eng. 30(12), 859–872 (2004)CrossRef

25.

Dhaussy, P., Teodorov, C.: Context-Aware Verification of a Landing Gear System. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 52–65. Springer International Publishing (2014)

26.

Falcone, Y., Havelund, K., Reger, G.: A Tutorial on Runtime Verification. In: Engineering Dependable Software Systems, volume 34 of NATO Science for Peace and Security Series—D: Information and Communication Security, pp. 141–175. IOS Press (2013)

27.

Farahbod, R., Glässer, U.: The CoreASM modeling framework. Softw., Pract. Exp. 41(2), 167–178 (2011)CrossRef

28.

Gargantini, A., Riccobene, E.: ASM-based testing: coverage criteria and automatic test sequence generation. J. Univ. Comput. Sci. 7, 262–265 (2001)

29.

Gargantini, A., Riccobene, E., Rinzivillo, S.: Using Spin to Generate Tests from ASM Specifications. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) Abstract State Machines 2003, volume of 2589 Lecture Notes in Computer Science, pp. 263–277. Springer, Berlin Heidelberg (2003)

30.

Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for abstract state machines. J. Univ. Comput. Sci. 14(12), 1949–1983 (2008)

31.

Glässer, U., Hallerstede, S., Leuschel, M., Riccobene, E.: Integration of tools for rigorous software construction and analysis (Dagstuhl Seminar 13372). Dagstuhl Rep. 3(9), 74–105 (2013)

32.

Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ Landing Gear System Using ProB. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study volume 433 of Communications in Computer and Information Science, pp. 66–79.Springer International Publishing (2014)

33.

Hierons, R., Derrick, J.: Editorial: special issue on specification-based testing. Softw. Test. Verif. Reliab. 10(4), 201–202 (2000)CrossRef

34.

Kossak, F.: Landing Gear System: An ASM-Based Solution for the ABZ Case Study. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 142–147. Springer International Publishing (2014)

35.

Laddad, R.: AspectJ in Action: Practical Aspect-Oriented Programming. Manning Publications Co., Greenwich, CT, USA (2003)

36.

Liang, H., Dong, J., Sun, J., Wong, W.: Software monitoring through formal specification animation. Innov. Syst. Soft. Eng. 5, 231–241 (2009)CrossRef

37.

Mammar, A., Laleau, R.: Modeling a Landing Gear System in Event-B. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 80–94. Springer International Publishing (2014)

38.

Méry, D., Singh, N. K.: Modeling an Aircraft Landing System in Event-B. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D., (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 154–159. Springer International Publishing (2014)

39.

Schellhorn, G.: Verification of ASM refinements using generalized forward simulation. J. Univ. Comput. Sci. 7(11), 952–979 (2001)MathSciNet

40.

Slissenko, A., Vasilyev, P.: Simulation of timed abstract state machines with predicate logic model-checking. J. Univ. Comput. Sci. 14(12), 1984–2006 (2008)MATH

41.

Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer (2001)

42.

Su, W., Abrial, J.-R.: Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System. In: Boniol, F., Wiels, V., Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 19–35. Springer International Publishing (2014)

43.

Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann, San Francisco, CA (2006)

44.

Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1–19:36 (2009)CrossRef

Titel: Rigorous development process of a safety-critical system: from ASM models to Java code
verfasst von: Paolo Arcaini
Angelo Gargantini
Elvinia Riccobene
Publikationsdatum: 04.08.2015
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 2/2017
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-015-0394-x

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 2/2017

The landing gear case study: challenges and experiments

Modeling a landing gear system in Event-B

The landing gear system in multi-machine Hybrid Event-B

Aircraft landing gear system: approaches with Event-B to the modeling of an industrial system

Environment-driven reachability for timed systems

Validation of the ABZ landing gear system using ProB