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
Software and Systems Modeling
Erschienen in: Software & Systems Modeling 3/2017

08.02.2016 | Regular Paper

Refinement-based Validation of Event-B Specifications

verfasst von: Atif Mashkoor, Faqing Yang, Jean-Pierre Jacquot

Erschienen in: Software and Systems Modeling | Ausgabe 3/2017

Einloggen

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

search-config
loading …

Abstract

The validation of formal specifications is a challenging task. It is one of the factors that impede the penetration of formal methods into the common practices of software development. This paper discusses the issue of validating formal models by executing them in the context of Event-B. The most important problem lies in the non-determinism which often prevents purely automatic tools to execute models. In this paper, we first present and discuss the techniques we have created to allow the execution of models at all levels of abstraction. These techniques rely on users to overcome the barriers resulting from non-deterministic features by either modifying the model or providing ad hoc implementations. Then, we present our main contribution, the formal definition of the notion of fidelity, that guarantees that all the observable behaviors of the executable models are indeed specified by the original (non-deterministic) models. The notion of fidelity can be expressed in terms of proof obligations.
Vorheriger Artikel A case study about the improvement of business process models driven by indicators
Nächster Artikel Design notations for secure software: a systematic literature review

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 "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

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
Fußnoten
1
“Prototypes” preexisting a software development are actually live specifications.
 
2
Provided the translators can be proven correct. While neither B2C nor EB2ALL is fully proven, they could be.
 
Literatur
1.
2.
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH
3.
Abrial, J.R.: From Z to B and then Event-B: assigning proofs to meaningful programs. In: Integrated Formal Methods. Lecture Notes in Computer Science, vol. 7940, pp. 1–15. Springer, Berlin (2013). doi:10.​1007/​978-3-642-38613-8_​1
4.
Abrial, J.R., Mussat, L.: Introducing dynamic constraints in B. In: B’98: Proceedings of the Second International B Conference on Recent Advances in the Development and Use of the B Method, pp. 83–128. Springer, London (1998)
5.
6.
Bendisposto, J., Leuschel, M., Ligot, O., Samia, M.: La validation de modèles Event-B avec le plug-in ProB pour RODIN. Tech. Sci. Inform. 27(8), 1065–1084 (2008)
7.
Bjørner, D.: Role of domain engineering in software development—why current requirements engineering is Flawed! In: Perspectives of Systems Informatics. Lecture Notes in Computer Science, vol. 5947, pp. 2–34. Springer, Berlin (2010)
8.
9.
Boulanger, J.L. (ed.): Industrial Use of Formal Methods: Formal Verification, Wiley Online Libray edn. Wiley, New York (2013)
10.
Broy, M., Slotosch, O.: Enriching the software development process by formal methods. In: Applied Formal Methods—FM-Trends 98. Lecture Notes in Computer Science, vol. 1641, pp. 44–61. Springer, Berlin (1999)
11.
12.
Daviet, P., Parent, M.: Longitudinal and lateral servoing of vehicles in a platoon. In: Proceedings of the IEEE Intelligent Vehicles Symposium, pp. 41–46 (1996)
13.
Deiters, W., Gruhn, V., Schäfer, W.: Systematic development of formal software process models. In: ESEC. Lecture Notes in Computer Science, vol. 387, pp. 100–117. Springer, Berlin (1989)
14.
DeRoever, W., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, New York (1999)
15.
Egyed, A.: Consistent adaptation and evolution of class diagrams during refinement. In: Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 2984, pp. 37–53. Springer, Berlin (2004). doi:10.​1007/​978-3-540-24721-0_​3
16.
Erasmy, F., Sekerinski, E.: RAISE: A rigorous approach using stepwise refinement. In: Formal Development of Reactive Systems. Lecture Notes in Computer Science, vol. 891, pp. 277–293. Springer, Berlin (1995)
17.
18.
Fowler, M.: UML Distilled: A Brief Guide to the Standard Object Modeling Language, 3rd edn. Addison-Wesley Longman Publishing Co. Inc, Boston (2003)
19.
Groslambert, J.: Verification of LTL on B-Event systems. In: B 2007: Formal Specification and Development in B. Lecture Notes in Computer Science, vol. 4355, pp. 109–124. Springer, Berlin (2006)
20.
Hoang, T.S., Abrial, J.R.: Reasoning about liveness properties in event-B. In: Qin, S., Qiu, Z. (eds.) Formal Methods and Software Engineering. Lecture Notes in Computer Science, vol. 6991, pp. 456–471. Springer, Berlin (2011)
21.
Hoare, C.: How did software get so reliable without proof? In: FME: Industrial benefit and advances in formal methods. Lecture Notes in Computer Science, vol. 1051, pp. 1–17. Springer, Berlin (1996)
22.
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)CrossRefMATH
23.
24.
Kossak, F., Mashkoor, A., Geist, V., Illibauer, C.: Improving the understandability of formal specifications: an experience report. In: Requirements Engineering: Foundation for Software Quality. Lecture Notes in Computer Science, vol. 8396, pp. 184–199. Springer International Publishing, Berlin (2014). doi:10.​1007/​978-3-319-05843-6_​14
25.
Kutzer, P., Gladigau, J., Haubelt, C., Teich, J.: Automatic generation of system-level virtual prototypes from streaming application models. In: 22nd IEEE International Symposium on Rapid System Prototyping, pp. 128–134 (2011). doi:10.​1109/​RSP.​2011.​5929986
26.
Martin, R.C.: Agile Software Development: Principles, Patterns, and Practices. Prentice Hall PTR, Upper Saddle River (2003)
27.
Mashkoor, A.: Formal Domain Engineering: From Specification to Validation. Ph.D. thesis, Université Nancy II (2011)
28.
Mashkoor, A., Biro, M., Dolgos, M., Timar, P.: Refinement-based development of software-controlled safety-critical active medical devices. In: Software Quality Days 2015. Lecture Notes in Business Information Processing, pp. 120–132. Springer International Publishing, Switzerland (2015)
29.
Mashkoor, A., Jacquot, J.P.: Stepwise validation of formal specifications. In: 18th Asia-Pacific Software Engineering Conference. Ho Chi Minh City, Vietnam (2011)
30.
Mashkoor, A., Jacquot, J.P.: Utilizing Event-B for domain engineering: a critical analysis. Requir. Eng. 16(3), 191–207 (2011)CrossRef
31.
Mashkoor, A., Jacquot, J.P.: Guidelines for formal domain modeling in Event-B. In: 16th IEEE International Symposium on High-Assurance Systems Engineering, pp. 158–165 (2015)
32.
Mashkoor, A., Jacquot, J.P., Souquières, J.: Transformation heuristics for formal requirements validation by animation. In: 2nd International Workshop on the Certification of Safety-Critical Software Controlled System, York, UK (2009)
33.
Mentré, D.: Checking temporal properties on state-based formal specification: application to railway level crossing. In: The 10th International Conference on Intelligent Transport Systems Telecommunications (2010)
34.
Méry, D., Singh, N.K.: Automatic code generation from Event-B models. In: Proceedings of the Second Symposium on Information and Communication Technology, pp. 179–188. ACM, New York (2011)
35.
36.
Milner, R.: A Calculus of Communicating Systems. Springer-Verlag New York Inc, Secaucus (1982)MATH
37.
Nakatani, T., Tsumaki, T., Tsuda, M., Inoki, M., Hori, S., Katamine, K.: Requirements maturation analysis by accessibility and stability. In: Software Engineering Conference, 18th Asia Pacific, pp. 357–364 (2011)
38.
Rushby, J.: Formal Methods and the Certification of Critical Systems. Technical Report CLS-93-7, Computer Science Laboratory—SRI International (1993)
39.
Savicks, V., Butler, M., Colley, J.: Co-simulation environment for Rodin: landing gear case study. In: ABZ 2014: The Landing Gear Case Study, Communications in Computer and Information Science, vol. 433, pp. 148–153. Springer International Publishing (2014). doi:10.​1007/​978-3-319-07512-9_​11
40.
41.
Servat, T.: BRAMA: a new graphic animation tool for B models. In: B 2007: Formal Specification and Development in B, pp. 274–276. Springer, Berlin (2006)
42.
Spivey, J.M.: The Z Notation: a Reference Manual. Prentice-Hall Inc, Upper Saddle River (1989)MATH
43.
Whalen, M., Cofer, D., Miller, S., Krogh, B.H., Storm, W.: Integration of formal analysis into a model-based software development process. In: Proceedings of the 12th International Conference on Formal Methods for Industrial Critical Systems, pp. 68–84. Springer, Berlin (2008)
44.
Wright, S., Eder, K.: Using Event-B to construct instruction set architectures. Form. Asp. Comput. 23(1), 73–89 (2011)CrossRef
45.
Yang, F.: A Simulation Framework for the Validation of Event-B Specifications. Ph.D. thesis, Université de Lorraine (2013)
46.
Yang, F., Jacquot, J.P.: Scaling up with Event-B: a case study. NASA Formal Methods. Lecture Notes in Computer Science, vol. 6617, pp. 438–452. Springer, Berlin (2011)
47.
Yang, F., Jacquot, J.P., Souquières, J.: The case for using simulation to validate Event-B specifications. In: Proceedings of 19th Asia-Pacific Software Engineering Conference, vol. 01, pp. 85–90. IEEE Computer Society, Washington (2012)
Metadaten
Titel
Refinement-based Validation of Event-B Specifications
verfasst von
Atif Mashkoor
Faqing Yang
Jean-Pierre Jacquot
Publikationsdatum
08.02.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 3/2017
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-016-0514-4

Weitere Artikel der Ausgabe 3/2017

Software & Systems Modeling 3/2017 Zur Ausgabe

Regular Paper

A graph-theoretic method for the inductive development of reference process models

Theme Section Paper

A visual language for modeling multiple perspectives of business process compliance rules

Theme Section Paper

Designing secure business processes with SecBPMN

Editorial

Theme section of BPMDS’2014: the human perspective in business processes

Theme Section Paper

Business processes in the agile organisation: a socio-technical perspective

Editorial

Logic formulas in models