A formal approach to AADL model-based software engineering

Formal methods have become a recommended practice in safety-critical software engineering. To be formally verified, a system should be specified with a specific formalism such as Petri nets, automata and process algebras, which requires a formal expertise and may become complex especially with large...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2020-04, Vol.22 (2), p.219-247
Main Authors: Mkaouar, Hana, Zalila, Bechir, Hugues, Jérôme, Jmaiel, Mohamed
Format: Article
Language:English
Subjects:
Computer Science
Engineering Sciences
Experimentation
Flight control systems
Mapping
Other
Petri nets
Preempting
Priority scheduling
Real time
Regular Paper
Safety critical
Software Engineering
Software Engineering/Programming and Operating Systems
Task scheduling
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Formal methods have become a recommended practice in safety-critical software engineering. To be formally verified, a system should be specified with a specific formalism such as Petri nets, automata and process algebras, which requires a formal expertise and may become complex especially with large systems. In this paper, we report our experience in the formal verification of safety-critical real-time systems. We propose a formal mapping for a real-time task model using the LNT language, and we describe how it is used for the integration of a formal verification phase in an AADL model-based development process. We focus on real-time systems with event-driven tasks, asynchronous communication and preemptive fixed-priority scheduling. We provide a complete tool-chain for the automatic model transformation and formal verification of AADL models. Experimentation illustrates our results with the Flight control system and Line follower robot case studies.
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-019-00513-7