The MODUS Approach to Formal Verification

• Authors: Lukasz Brewka , José Soler , Michael Berger
• Languages of publication: EN

Abstracts

EN

Background: Software reliability is of great importance for the development of embedded systems that are often used in applications that have requirements for safety. Since the life cycle of embedded products is becoming shorter, productivity and quality simultaneously required and closely in the process of providing competitive products Objectives: In relation to this, MODUS (Method and supporting toolset advancing embedded systems quality) project aims to provide small and medium-sized businesses ways to improve their position in the embedded market through a pragmatic and viable solution Methods/Approach: This paper will describe the MODUS project with focus on the technical methodologies that can assist formal verification and formal model checking. Results: Based on automated analysis of the characteristics of the system and by controlling the choice of the existing opensource model verification engines, model verification producing inputs to be fed into these engines. Conclusions: The MODUS approach is aligned with present market needs; the familiarity with tools, the ease of use and compatibility/interoperability remain among the most important criteria when selecting the development environment for a project

Keywords

EN

software quality; formal verification; embedded systems; translation tool selection

• Publisher: Sciendo
• Journal: Business Systems Research Journal
• Year: 2014
• Volume: 5
• Issue: 1
• Pages: 21-33

Dates

published

2014-03-01

online

2014-04-23

Contributors

author

Lukasz Brewka

• DTU Fotonik, Denmark

author

José Soler

• DTU Fotonik, Denmark

author

Michael Berger

• DTU Fotonik, Denmark

References

• 1. George, C. (2008), “RAISE Tool User Guide”, available at: http://www.iist.unu.edu/newrh/III/3/1/docs/rsltc/user_guide/html/ug.html (12 September 2012).
• 2. Haxthausen, A. (2010), Lecture notes, 02263 Formal Aspects of Software Engineering, available at http://www2.imm.dtu.dk/courses/02263/F14/index/ / (10 September 2012)
• 3. Holzmann, G. J. (2003), The Spin Model Checker: Primer and Reference Manual, Boston: Addison-Wesley.
• 4. Knapp, A. (2008), ”Hugo/RT”, available at: http://www.pst.ifi.lmu.de/projekte/hugo / (12 September 2012).
• 5. Meenakshi, B. (2004), A tutorial on SPIN, Bangalore: Honeywell Technology Solutions Lab.
• 6. MODUS (2013a), Deliverable D2.1 “State-of-the-art review and identification of technological requirements”, Internal documentation.
• 7. MODUS (2013b), Deliverable D2.2 “MODUS functional and technical specifications”, Internal documentation.
• 8. MODUS (2013c), Deliverable D3.1 “Methodological framework for LNR-based model transformation and code generation”, Internal documentation.
• 9. MODUS (2013d), Deliverable D3.2 “LNR-based model transformation and code generation modules”, Internal documentation.
• 10. Schäfer, T., Knapp, A., Merz, S. (2001), “Model Checking UML State Machines and Collaborations”, Electronic Notes in Theoretical Computer Science, Vol. 55, No. 3, pp. 357-369.

Identifiers

DOI

10.2478/bsrj-2014-0002