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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Programming and Computer Software
Erschienen in: Programming and Computer Software 5/2023

01.10.2023

Automata-Based Software Engineering with Event-B

verfasst von: V. I. Shelekhov

Erschienen in: Programming and Computer Software | Ausgabe 5/2023

Einloggen

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

search-config
loading …

Abstract

A new automata-based programming language built by extending the Event-B specification language is proposed. When developing models in Event-B, it becomes possible to use automata-based methods in addition to the popular refinement method. The automata-based software engineering based on Event-B is demonstrated by the example of traffic control on a bridge from the Event-B system manual. A simpler solution with verification in the Rodin tool is proposed. The effectiveness of Event-B verification methods is confirmed by finding three nontrivial bugs in our solution.
Vorheriger Artikel Metaclasses in UML and in Programming Languages

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

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+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
Fußnoten
Literatur
1.
Abrial, J.-R., Modeling in Event-B: System and Software Engineering, Cambridge: Cambridge Univ. Press, 2010.CrossRefMATH
2.
Rodin User’s Handbook, Version 2.8, Ed. by Jastram, M., 2014.
3.
Butler, M.J., Körner, P., Krings, S., Lecomte, T., Leuschel, M., Mejia, L.-F., and Voisin, L., The first twenty-five years of industrial use of the B-Method, in Formal Methods for Industrial Critical Systems (FMICS), 2020, pp. 189–209.
4.
Kharnaukhov, N., Perchine, D., and Shelekhov, V., The Predicate Programming Language P, Novosibirsk: Inst. Sistem Informatiki, Sib. Otd. Russ, Akad. Nauk, 2018 [in Russian]. http://persons.iis.nsk.su/files/persons/pages/plang14.pdf . Accessed February 9, 2022.
5.
Shelekhov, V.I., Automata-based software engineering: The language and development methods. Program. Ingeneriya, 2014, No. 4, pp. 3–15. http://persons.iis.nsk.su/files/persons/pages/automatProg.pdf. Accessed February 9, 2022.
6.
Tumurov, E.G. and Shelekhov, V. I., Applying automata-based software engineering for the elevator control program, Program. Ingeneriya, 2017, vol. 8, no. 4, pp. 99–111. http://​persons.​iis.​nsk.​su/​files/​persons/​pages/​lift1.​pdf.​ Accessed February 9, 2022.
7.
Shelekhov, V.I., Automata-based programming on the basis of requirement specifications, System Informatics, 2015, no. 1, pp. 1–29. http://persons.iis.nsk.su/files/persons/pages/req_tech.pdf. Accessed February 9, 2022.
8.
Shelekhov, V.I., Automata-based program optimization by applying requirement transformations, Program. Inzheneriya, 2015, no. 11, pp. 3–13. http://persons.iis.nsk.su/files/persons/pages/req_k.pdf. Accessed February 9, 2022.
9.
Hoare, C.A. R., An axiomatic basis for computer programming, Commun. ACM, 1969, vol. 12, no. 10, pp.576–585.CrossRefMATH
10.
Floyd, R.W., Assigning meanings to programs. Proc. of the Symposium in Applied Mathematics, Mathematical Aspects of Computer Science, AMS, 1967. pp. 19–32.
11.
Shelekhov, V.I., Program classification in software engineering, Program. Ingeneriya, 2016, vol. 7, no. 12, pp. 531–538. https://persons.iis.nsk.su/files/persons/pages/prog.pdf. Accessed February 9, 2022.
12.
Liskov, B. and Zilles, S., Programming with abstract data types, Proc. of the ACM SIGPLAN Symposium on Very High Level Languages, SIGPLAN Notices, 1974, vol. 9, pp. 50–59.CrossRef
13.
Systems and software engineering — Life cycle processes — Requirements engineering. ISO/IEC/ IEEE 29148, 2011.
14.
Shelekhov, V.I., Development of a program for building a suffix tree in the predicate software engineering, Preprint of Institute of Informatics Systems, Novosibirsk, 2004, no. 115, 52p.
15.
Shelekhov, V., Development and verification of the heapsort algorithms using the predicate programming technology, Preprint of Institute of Informatics Systems, Novosibirsk, 2012, no. 164, 30 p.
16.
Owre, S., Rushby, J.M., and Shankar, N., PVS: Specification and Verification System. CADE-11: Automated Deduction. Lect. Notes Comput. Sci., 1992, vol. 607, p. 748–752.CrossRef
17.
Why 3. Where Programs Meet Provers, available at: http://​why3.​lri.​fr.​ Accessed February 9, 2022.
18.
The Coq Proof Assistant, available at http://​coq.​inria.​fr.​ Accessed February 9, 2022.
19.
Shelekhov, V.I., Comparison of automata-based engineering method and Event-B modeling metho, Sist. Inform., 2021, no. 18, pp. 53–84. https://persons.iis.nsk.su/files/persons/pages/bridge.pdf. Accessed February 9, 2022.
20.
Shalyto, A.A., SWITCH-technology: Algorithmic and Programming Methods in Solution of Logic Control Problems, St. Petersburg: Nauka, 1998 [in Russian]. http://​is.​ifmo.​ru/​books/​switch/​1.​ Accessed February 9, 2022.
21.
Specification and description language (SDL). ITU-T Recommendation Z.100 (03/93). http://www.itu.int/ITU-T/studygroups/com17/languages/Z100.pdf. Accessed February 9, 2022.
22.
Lamport, L., Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley, 2021.
23.
Parondzanov, V.D., DRAKON Language: Short Description, Moscow: 2009 [in Russian]. http://​drakon.​su/​_​media/​biblioteka/​drakondescriptio​n.​pdf.​ Accessed February 9, 2022.
24.
Polykarpova, N.I. and Shalyto, A.A., Automata-Based Programming, 2nd ed., St. Petersburg: Piter, 2020 [in Russian].
25.
Hoang, T.S., Dghaym, D., Snook, C., and Butler, M., A composition mechanism for refinement-based methods, 22nd Int. Conference on Engineering of Complex Computer Systems (ICECCS), 2017, pp. 100–109.
26.
Abrial, J.-R., The B-book—Assigning Programs to Meanings, Cambridge Univ. Press, 2005.MATH
27.
Milner, R., Communication and Concurrency. International Series in Computer Science, Prentice Hall, 1989.
28.
Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall Int., 1985.MATH
29.
Larson, J., Erlang for concurrent programming, ACM Queue, 2008, No. 5, pp. 18–23.
30.
Nicola, R.D., Duong, T., and Inverso, O., Verifying AbC specifications via emulation. leveraging applications of formal methods, verification and validation: Engineering principles, ISoLA, Part II, Lect. Notes Comput. Sci., 2020, vol. 12477, pp. 261–279.
31.
Liu, P., Wahl, T., and Lal, A., Verifying asynchronous event-driven programs using partial abstract transformers. Computer Aided Verification, Lect. Notes Comput. Sci., 2019, vol. 11562, pp. 386–404.CrossRef
32.
Desai, A., Qadeer, S., and Seshia, S.A., Programming safe robotics systems: Challenges and advances. Leveraging Applications of Formal Methods, Verification and Validation. Verification, Lect. Notes Comput. Sci., 2018, vol. 11245, pp. 103–119.
33.
Ferg, S., Event-Driven Programming: Introduction, Tutorial, History, SourceForge, 2006.
Metadaten
Titel
Automata-Based Software Engineering with Event-B
verfasst von
V. I. Shelekhov
Publikationsdatum
01.10.2023
Verlag
Pleiades Publishing
Erschienen in
Programming and Computer Software / Ausgabe 5/2023
Print ISSN: 0361-7688
Elektronische ISSN: 1608-3261
DOI
https://doi.org/10.1134/S0361768823050079

Weitere Artikel der Ausgabe 5/2023

Programming and Computer Software 5/2023 Zur Ausgabe

OriginalPaper

Searching for Laurent Solutions of Systems of Linear Differential Equations with Truncated Power Series in the Role of Coefficients

OriginalPaper

Complementarity in Finite Quantum Mechanics and Computer-Aided Computations of Complementary Observables

OriginalPaper

Database Migration from ORACLE to PostgreSQL

OriginalPaper

Metaclasses in UML and in Programming Languages

OriginalPaper

Automated Verification of Multi-Party Agreements and Scheduling of Sending Messages in Distributed Ledger Systems

OriginalPaper

On Implementation of Numerical Methods for Solving Ordinary Differential Equations in Computer Algebra Systems

Premium Partner

    Bildnachweise