nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Model-Driven Re-engineering of a Pressure Sensing System: An Experience Report

verfasst von : Atif Mashkoor, Felix Kossak, Miklós Biró, Alexander Egyed

Erschienen in: Modelling Foundations and Applications

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

This article presents our experience in re-engineering a pressure sensing system – a subsystem often found in safety-critical medical devices – using the B formal method. We evaluate strengths and limitations of the B method and its supporting platform Atelier B in this context. We find that the current state-of-the-art of model-oriented formal methods and associated tool-sets, especially in automatic code generation, requires further improvement to be amenable to a wider deployment to industrial applications for model-driven engineering purposes.

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

Vorheriges Kapitel Towards a Framework for Writing Executable Natural Language Rules

Nächstes Kapitel Modeling AUTOSAR Implementations in Simulink

http://www.mathworks.com/products/simulink.

http://www.estereltechnologies.com/products/scade-suite.

http://www.atelierb.eu.

According to ClearSy, they will fix some of the concerns raised in this paper in the upcoming version of the code generator.

According to ClearSy, in the upcoming version of the code generator, custom identifiers (without prefix) would be possible. This would indeed constitute a major improvement and should be regarded as an important and feasible requirement for code generators.

According to ClearSy, this construct eases the proving process.

Atelier B Translators: User Manual version 4.6. http://tools.clearsy.com/resources/documents. Accessed 28 Feb 2018

Abrial, J.R.: The B Book. Cambridge University Press, Cambridge (1996)CrossRef

Abrial, J.R.: Formal methods in industry: achievements, problems, future. In: Proceedings of the 28th International Conference on Software Engineering ICSE 2006, pp. 761–768. ACM, New York (2006)

Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRef

Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2015, pp. 80–89. Austin, 21–23 September 2015

Benveniste, M.: On using B in the design of secure micro-controllers: an experience report. Electron. Notes Theor. Comput. Sci. 208, 3–22 (2011)CrossRef

Bert, D., Boulmé, S., Potet, M.-L., Requet, A., Voisin, L.: Adaptable translator of B specifications to embedded C programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 94–113. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_7CrossRef

Börger, E., Stark, R.F.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag New York Inc., Secaucus (2003)CrossRef

Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28(4), 626–643 (1996)CrossRef

10.

Daskaya, I., Huhn, M., Milius, S.: Formal safety analysis in industrial practice. In: Salaün, G., Schätz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 68–84. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24431-5_7CrossRef

11.

Edmunds, A., Butler, M., Maamria, I., Silva, R., Lovell, C.: Event-B code generation: type extension with theories. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 365–368. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30885-7_33CrossRef

12.

Fitzgerald, J.S., Larsen, P.G.: Triumphs and challenges for model-oriented formal methods: the VDM++ experience. In: Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2006), pp. 1–4, November 2006

13.

Fürst, A., Hoang, T.S., Basin, D., Desai, K., Sato, N., Miyazaki, K.: Code generation for Event-B. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 323–338. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10181-1_20CrossRef

14.

Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge (2006)

15.

Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall Inc., Upper Saddle River (1990)MATH

16.

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. CCIS, vol. 433, pp. 142–147. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07512-9_10CrossRef

17.

Kossak, F., Mashkoor, A.: How to select the suitable formal method for an industrial application: a survey. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 213–228. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_13CrossRef

18.

Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)

19.

Lecomte, T.: Atelier B has turned twenty. In: Keynote of the Fifth International Conference on ASMs, Alloy, B, TLA, VDM, and Z (ABZ 2016). Springer, Heidelberg (2016)

20.

Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRef

21.

Mashkoor, A.: The hemodialysis machine case study. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 329–343. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_29CrossRef

22.

Mashkoor, A.: Model-driven development of high-assurance active medical devices. Softw. Q. J. 24(3), 571–596 (2016). https://doi.org/10.1007/s11219-015-9288-0CrossRef

23.

Mashkoor, A., Biro, M.: Towards the trustworthy development of active medical devices: a hemodialysis case study. IEEE Embed. Syst. Lett. 8(1), 14–17 (2016)CrossRef

24.

Mashkoor, A., Biro, M., Dolgos, M., Timar, P.: Refinement-based development of software-controlled safety-critical active medical devices. In: Winkler, D., Biffl, S., Bergsmann, J. (eds.) SWQD 2015. LNBIP, vol. 200, pp. 120–132. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-13251-8_8CrossRef

25.

Mashkoor, A., Hasan, O., Beer, W.: Using probabilistic analysis for the certification of machine control systems. In: Cuzzocrea, A., Kittl, C., Simos, D.E., Weippl, E., Xu, L. (eds.) CD-ARES 2013. LNCS, vol. 8128, pp. 305–320. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40588-4_21CrossRef

26.

Méry, D., Singh, N.K.: Automatic code generation from Event-B models. In: Proceedings of the Second Symposium on Information and Communication Technology SoICT 2011, pp. 179–188. ACM, New York (2011)

27.

Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM 53(2), 58–64 (2010)CrossRef

28.

Reicherdt, R., Glesner, S.: Formal verification of discrete-time MATLAB/Simulink models using boogie. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 190–204. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10431-7_14CrossRef

29.

Spivey, J.M.: Understanding Z: A Specification Language and Its Formal Semantics. Cambridge University Press, Cambridge (1988)MATH

30.

Wright, S.: Automatic generation of C from Event-B. In: Workshop on Integration of Model-based Formal Methods and Tools (2009)

Titel: Model-Driven Re-engineering of a Pressure Sensing System: An Experience Report
verfasst von: Atif Mashkoor
Felix Kossak
Miklós Biró
Alexander Egyed
Verlag: Springer International Publishing
Buch: Modelling Foundations and Applications
Print ISBN: 978-3-319-92996-5

Electronic ISBN: 978-3-319-92997-2

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-92997-2_17

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"