nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

16.05.2018 | Introduction

Formal methods and automated verification of critical systems

verfasst von: Maurice H. ter Beek, Stefania Gnesi, Alexander Knapp

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

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Critical (software) systems are all around us. These systems are typically characterised by stringent dependability requirements and demand elevated levels of robustness and fault tolerance. To assure that they function as intended and provide a number of quality guarantees, formal methods and automated verification techniques and tools have been in use in the engineering of such critical systems for many years now. In this introduction to the special issue FMICS–AVoCS on “Formal Methods and Automated Verification of Critical Systems”, we outline a number of recent achievements concerning the use of formal methods and automated verification techniques and tools for the specification and analysis of critical systems from a variety of application domains. These achievements are represented by six selected papers: five were selected from the joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems (FMICS–AVoCS 2016), while one of them was selected after an open call for papers.

Nächster Artikel Qualitative and quantitative analysis of safety-critical systems with

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

S3 is developed, maintained and distributed by Systerel.

http://sicstus.sics.se/

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

Gnesi, Stefania, Margaria, Tiziana (eds.): Formal Methods for Industrial Critical Systems: A Survey of Applications. John Wiley & Sons Inc, Hoboken (2013)

ter Beek, M.H., Clarke, D., Schaefer, I.: Editorial preface for the JLAMP special issue on formal methods for software product line engineering. J. Log. Algebraic Methods Programm. 85(1), 123–124 (2016)CrossRefMATH

ter Beek, M.H., Lisitsa, A., Nemytykh, A.P., Ravara, A.: Automated verification of programs and Web systems. J. Log. Algebraic Methods Programm. 85(5), 653–654 (2016)MathSciNetCrossRefMATH

ter Beek, M.H., Lafuente, A.L.: Automated specification and verification of Web-based applications. J. Log. Algebraic Methods Program. 87, 51 (2017)MathSciNetCrossRefMATH

Güdemann, M., Núñez, M.: Preface of the special issue on formal methods in industrial critical systems. Int. J. Softw. Tools Technol. Transf. 19(4), 391–393 (2017)CrossRef

Ozay, N., Tabuada, P.: Guest editorial: special issue on formal methods in control. Discrete Event Dyn. Syst. 27(2), 205–208 (2017)MathSciNetCrossRefMATH

Grov, G., Ireland, A.: Preface of the special issue on automated verification of critical systems (AVoCS 2015). Sci. Comput. Program. 148, 1–2 (2017)CrossRef

ter Beek, M.H., Loreti, M.: Guest editorial for the special issue on formal methods for the quantitative evaluation of collective adaptive systems (FORECAST). ACM Trans. Model. Comput. Simul. 28(2), 81–84 (2018)MathSciNet

10.

ter Beek, M.H., Gnesi, S., Knapp, A.: Formal methods for transport systems. Int. J. Softw. Tools Technol. Transf. 20(3), 237–241 (2018)CrossRef

11.

Almeida, J.B., Frade, M.J., Pinto, J.S., de Sousa, S.M.: An overview of formal methods tools and techniques. In: Rigorous Software Development. Undergraduate Topics in Computer Science, pp. 15–44. Springer, London (2011)

12.

ter Beek, M.H., Gnesi, S., Knapp, A. (eds.): Critical systems: formal methods and automated verification. In: Proceedings of the Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS 2016), volume 9933 of Lecture Notes in Computer Science. Springer (2016)

13.

Leupolz, J., Knapp, A., Habermaier, A., Reif, W.: Qualitative and quantitative analysis of safety-critical systems with S#. Int. J. Softw. Tools Technol. Transf. (2018). In this issue

14.

Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: High-performance language-independent model checking. In: Baier, C, Tinelli, C (eds.) Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), volume 9035 of Lecture Notes in Computer Science, pp. 692–707. Springer (2015)

15.

de Pedro, M.A.., Sousa Pinto, J., Pereira, D., Pinho, L.M.: Runtime verification of autopilot systems using a fragment of MTL-\({\int }\). Int. J. Softw. Tools Technol. Transf. (2018). In this issue

16.

Chadli, M., Kim, J.H., Larsen, K.G., Legay, A., Naujokat, S., Steffen, B., Traonouez, L.-M.: High-level frameworks for the specification and verification of scheduling problems. Int. J. Softw. Tools Technol. Transfer (2018). In this issue

17.

David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397–415 (2015)CrossRef

18.

Ge, N., Jenn, E., Breton, N., Fonteneau, Y.: Integrated formal verification of safety-critical software. Int. J. Softw. Tools Technol. Transf. (2018). In this issue

19.

Clabaut, M., Ge, N., Breton, N., Jenn, E., Delmas, R., Fonteneau, Y.: Industrial grade model checking—use cases, constraints, tools and applications. In: Proceedings of the 8th European Congress on Embedded Real Time Software and Systems (ERTS\(^2\) 2016), pp. 85–92 (2016).

20.

Huang, W.L., Peleska, J.: Model-based testing strategies and their (in)dependence on syntactic model representations. Int. J. Softw. Tools Technol. Transf. (2018). In this issue

21.

Bride, H., Kouchnarenko, O., Peureux, F., Voiron, G.: Assessing SMT and CLP approaches for workflow nets verification. Int. J. Softw. Tools Technol. Transf. (2018). In this issue

22.

de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), volume 4963 of Lecture Notes in Computer Science, pp. 337–340. Springer (2008)

23.

Carlsson, M., Mildner, P.: SICStus prolog-The first 25 years. Theory Pract. Logic Program. 12(1–2), 35–66 (2012)MathSciNetCrossRefMATH

Titel: Formal methods and automated verification of critical systems
verfasst von: Maurice H. ter Beek
Stefania Gnesi
Alexander Knapp
Publikationsdatum: 16.05.2018
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 4/2018
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-018-0494-5

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 4/2018

Model-based testing strategies and their (in)dependence on syntactic model representations

Integrated formal verification of safety-critical software

High-level frameworks for the specification and verification of scheduling problems

Runtime verification of autopilot systems using a fragment of MTL-

Assessing SMT and CLP approaches for workflow nets verification

Qualitative and quantitative analysis of safety-critical systems with