Project description

Compositional Verification of Real-time MULTI-CORE SAFETY Critical Systems (Part of project application)

Safety critical real-time systems are a vital component in modern cars, self-driving cars, trains,
planes and many industrial machines. Many resources are used to verify the correct operation of
such systems as malfunctioning software can lead to great harm or death. The functionality of such
embedded systems are divided into tasks that have to complete before a strict deadline. Classical
schedulability analysis can determine whether all tasks will always meet their deadlines. This is done
with very little information about the individual tasks behavior. Modern CPUs are based on multi-
core architectures. In order to be able to use multi-core processors in safety-critical applications it is
essential that we can analyze the behavior of the complete safety critical system including the com-
munication between tasks running on different cores. Classical schedulability analysis techniques are
pessimistic in their assumptions in order to ensure the safe operation of the systems. International
safety related standards, such as ISO 26262 and IEC 61508, emphasize the use of formal methods in
creating systems with very high reliability. Through EU projects RECOMP and CRAFTERS the ap-
plicant has witnessed the industrial need for usable formal methods, but also the scalability problems
that current methods suffer from. Compositional verification is one of the most promising techniques
when it comes to handling full size industrial systems, and could thus help bridge the gap between
formal methods

[22], will be defined and made available as a tool.
Project Objectives: The goal of MULTI-CORE-SAFETY can be stated as:
To take a giant leap forward in schedulability analysis for multi-core architectures; analyzing
industrial sized systems with more accuracy and flexibility through the use of compositional
model checking techniques.

Problem: Classical Schedulability Analysis is too Pessimistic: Classical schedulability analy-
sis methods are too pessimistic in which systems are deemed schedulable. The problem is that either
multi-core systems cannot be used in safety-critical applications or if used the resources that they
provide would be severely under utilized in order to ensure the safe operation of the system. Classical
schedulability theories have been developed for multi-core systems, but these theories do not handle
the communication between the tasks and locking of resources in a very detailed manner, which leads
to sub-optimal use of system resources.
Suggested Solution: In order to remedy this the applicant proposes to use compositional verifica-
tion techniques for timed systems to analyze detailed models of multi-core scheduling systems. A tool
will be developed for specifying task behavior and system architecture. From this Timed Input/Output
Automata models will be automatically generated and analyzed.
Hypothesis: The research proposed in MULTI-CORE-SAFETY is centered around the follow-
ing hypothesis.
A compositional model-based approach can enable detailed, automatic and accurate analysis of
industrial multi-core scheduling systems.
State of the Art in Schedulability Analysis: Most research within the schedulability research
community is still based on the classical notion of task interfaces [14]. Using this notion almost no
behavioral information about the internal working of the task is included in the schedulability analy-
sis. The most basic concept of task as used in scheduling systems is a form of interface description of
a part of the system. Compositional analysis of multi-core scheduling systems using classical meth-
ods [20, 21] have, among others, been advocated by Insup Lee. Such techniques allow for modular
design and separation of concerns, but will in general not utilize system resources optimally.
The authors of [10] provided a compositional framework for the verification of hierarchical
scheduling systems using a model-based approach. They specified the system behavior in terms of
preemptive time Petri nets, and only considered a single-core execution platform. I strongly believe
that an automata based modeling and verification approach is more suited to easily describe any
potential scheduling system. Model checking techniques have been applied to the verification of
scheduling system. In these examples there have been a great degree of tailoring of the models to the
specific system [12, 3, 5].
Scientific Novelty: MULTI-CORE-SAFETY represents a novel composition of compositional
verification techniques and schedulability analysis. The potential for significantly influencing the
field of schedulability analysis is huge. In [13] experimental results are presented demonstrating that
for certain types of systems compositional model checking can be several orders of magnitude faster
than non-compositional verification. Compositional verification also has the advantage of leading to
2modular systems design and natural separation of concerns.
A lot of the research that is presented within the schedulability community lack real industrial
case-studies. En order to remedy this MULTI-CORE-SAFETY includes an industrial partner
which can provide such a case study and validate the relevance of the results.
Outcome of the Project More exact and scalable analysis for multi-core scheduling systems,
disseminated through publications and tools for schedulability analysis.
The Practical Feasibility of the Project: To ensure the relevance for the schedulability commu-
nity and an aligment with the most recent trends in the schedulability community, extensive coopera-
tion with the research group of Professor Insup Lee from the University of Pennsylvania will be part
of MULTI-CORE-SAFETY. The cooperation will be ensured through monthly video conferences,
yearly visits by researchers from University of Pennsylvania, and a three months external stay by
the PhD student. Insup Lee has worked extensively with certification of software for medical prod-
ucts under the US FDA (Food and Drug Administration). To ensure the relevance of the developed
schedulability tool as a vehicle for further research for other research groups, the project will also
include Axel Legay the leader of the ESTASYS (Efficient STAtistical methods in SYstems of Systems)
research team at INRIA Rennes.
To ensure the industrial relevance and applicability of the project, cooperation has been ensured
with the Danish industrial company Grundfos (www.grundfos.com). Grundfos Group has more than
18,000 employees worldwide and produces more than 16 million pump units per year. Their products
have a very long lifetime and thus need extremely high operating reliability. The main role of Grundfos
in the project is to provide a realistic case study.
The major part of the budget will provide funding for a PhD student, who together with the appli-
cant will be involved in all aspects of the project.
Hiring: The call for the PhD scholarship will be made together with a common call made by the de-
partment of computer science. The call will be widely advertised in the verification and schedulability
communities. The research unit has a history of attracting strong candidates.

Work Packages:
The research will be divided into three work packages.
WP1 – Modeling and semantics: Focusing on creating generic models needed for the automatic
translation and on defining a flexible specification language with a formal semantics.
WP2 – Tool development: Focusing a developing a robust tool implementation for the automatic
model translation and analysis using the back-end tool Ecdar.
WP3 – Evaluation: Focusing on evaluation of the developed tool on a realistic industrial case-study.

 

References
[1] Sebastian S. Bauer, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. A modal
specification theory for components with data. Sci. Comput. Program., 83:106–128, 2014.
[2] Gerd Behrmann, Alexandre David, and Kim Guldstrand Larsen. A tutorial on uppaal. In
Marco Bernardo and Flavio Corradini, editors, Formal Methods for the Design of Real-Time
Systems, International School on Formal Methods for the Design of Computer, Communica-
tion and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised
Lectures, volume 3185 of Lecture Notes in Computer Science, pages 200–236. Springer, 2004.
[3] Abdeldjalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim. G. Larsen, Marius Mikučionis,
Ulrik Nyman, and Arne Skou. Hierarchical scheduling framework based on compositional anal-
ysis using uppaal. In Proceedings of FACS 2013, lncs. Springer, 2013. To appear.
[4] Abdeldjalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim G. Larsen, Marius Mikucionis, Ul-
rik Nyman, and Arne Skou. Statistical and exact schedulability analysis of hierarchical schedul-
ing systems. Sci. Comput. Program., 127:103–130, 2016.
[5] Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Ulrik Nyman, Marius
Mikucionis, and Arne Skou. Widening the schedulability hierarchical scheduling systems. In
Proceedings of FACS 2014, 2014.
[6] Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Ulrik Nyman, and
Arne Skou. Schedulability and energy efficiency for multi-core hierarchical scheduling systems.
In Proceedings of ERTS2 2014, 2014.
[7] Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Ulrik Nyman, Arne
Skou, and Marius Mikucionis. Degree of schedulability of mixed-criticality real-time systems
with probabilistic sporadic tasks. In Proceedings of TASE 2014, 2014.
[8] Jalil Boudjadar, Jin Hyun Kim, Kim Guldstrand Larsen, and Ulrik Nyman. Model checking
process algebra of communicating resources for real-time systems. In Proceedings of ECRTS
2014, 2014.
[9] Jalil Boudjadar, Kim Guldstrand Larsen, Jin Hyun Kim, and Ulrik Nyman. Compositional
schedulability analysis of an avionics system using uppaal. In ICAASE 2014, 2014.
[10] Laura Carnevali, Alessandro Pinzuti, and Enrico Vicario. Compositional verification for hierar-
chical scheduling of real-time systems. IEEE Transactions on Software Engineering, 39(5):638–
657, 2013.
[11] Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. Timed I/O
automata: a complete specification theory for real-time systems. In Karl Henrik Johansson and
Wang Yi, editors, Proceedings of the 13th ACM International Conference on Hybrid Systems:
Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010, pages 91–100.
ACM, 2010.
[12] Alexandre David, Kim Guldstrand Larsen, Axel Legay, and Marius Mikučionis. Schedulability
of herschel-planck revisited using statistical model checking. In ISoLA (2), volume 7610 of
LNCS, pages 293–307. Springer, 2012.
[13] Alexandre David, Kim Guldstrand Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski.
ECDAR: an environment for compositional design and analysis of real time systems. In Ahmed
Bouajjani and Wei-Ngan Chin, editors, Automated Technology for Verification and Analysis
– 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings,
volume 6252 of Lecture Notes in Computer Science, pages 365–370. Springer, 2010.
[14] Robert I. Davis and Alan Burns. A survey of hard real-time scheduling for multiprocessor
systems. ACM Comput. Surv., 43(4):35:1–35:44, October 2011.
[15] Kim G. Larsen, Ulrik Nyman, and Andrzej W asowski. Interface input/output automata: Splitting
assumptions from guarantees. ENTCS. Elsevier Science Publishers, 2005.
[16] Kim Guldstrand Larsen, Ulrik Nyman, and Andrzej Wasowski. Interface input/output automata.
In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM, volume 4085 of Lecture
Notes in Computer Science, pages 82–97. Springer, 2006.
[17] Kim Guldstrand Larsen, Ulrik Nyman, and Andrzej W asowski. Modal i/o automata for interface
and product line theories. In Rocco De Nicola, editor, ESOP, volume 4421 of Lecture Notes in
Computer Science, pages 64–79. Springer, 2007.
[18] Kim Guldstrand Larsen, Ulrik Nyman, and Andrzej Wasowski.
On modal refinement and consistency. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR, volume 4703 of
Lecture Notes in Computer Science, pages 105–119. Springer, 2007.
[19] Safety Integrity Levels. https://en.wikipedia.org/wiki/safety_integrity_level.
[20] Insik Shin and Insup Lee. Periodic resource model for compositional real-time guarantees. In
RTSS, pages 2–13. IEEE Computer Society, 2003.
[21] Insik Shin and Insup Lee. Compositional real-time scheduling framework with periodic model.
ACM Trans. Embedded Comput. Syst., 7(3), 2008.
[22] Ecdar tool website. http://ecdar.cs.aau.dk.

and software engineering practice.
Classical schedulability analysis [20] although safe can be too pessimistic, because of classical
task models lacking detailed behavior, thus leading to an under-utilization of system resources. Au-
tomata based models of scheduling systems provide a basis for more detailed and accurate analysis
of scheduling systems, including multi-core systems.
The idea behind MULTI-CORE-SAFETY comes from a realization that compositional analysis
strategies used for schedulability analysis [3] is a perfect fit with the type of compositional analysis of
timed systems the applicant developed in [11]. More recently the applicant has suggested a modeling
formalism for heterogeneous multi-core scheduling systems in [4]. In MULTI-CORE-SAFETY
an exact semantic translation from this modeling formalism into Timed Input/Output Automata, as
defined by Ecdar[22], will be defined and made available as a tool.
Project Objectives: The goal of MULTI-CORE-SAFETY can be stated as:
To take a giant leap forward in schedulability analysis for multi-core architectures; analyzing
industrial sized systems with more accuracy and flexibility through the use of compositional
model checking techniques.

Problem: Classical Schedulability Analysis is too Pessimistic: Classical schedulability analy-
sis methods are too pessimistic in which systems are deemed schedulable. The problem is that either
multi-core systems cannot be used in safety-critical applications or if used the resources that they
provide would be severely under utilized in order to ensure the safe operation of the system. Classical
schedulability theories have been developed for multi-core systems, but these theories do not handle
the communication between the tasks and locking of resources in a very detailed manner, which leads
to sub-optimal use of system resources.
Suggested Solution: In order to remedy this the applicant proposes to use compositional verifica-
tion techniques for timed systems to analyze detailed models of multi-core scheduling systems. A tool
will be developed for specifying task behavior and system architecture. From this Timed Input/Output
Automata models will be automatically generated and analyzed.
Hypothesis: The research proposed in MULTI-CORE-SAFETY is centered around the follow-
ing hypothesis.
A compositional model-based approach can enable detailed, automatic and accurate analysis of
industrial multi-core scheduling systems.
State of the Art in Schedulability Analysis: Most research within the schedulability research
community is still based on the classical notion of task interfaces [14]. Using this notion almost no
behavioral information about the internal working of the task is included in the schedulability analy-
sis. The most basic concept of task as used in scheduling systems is a form of interface description of
a part of the system. Compositional analysis of multi-core scheduling systems using classical meth-
ods [20, 21] have, among others, been advocated by Insup Lee. Such techniques allow for modular
design and separation of concerns, but will in general not utilize system resources optimally.
The authors of [10] provided a compositional framework for the verification of hierarchical
scheduling systems using a model-based approach. They specified the system behavior in terms of
preemptive time Petri nets, and only considered a single-core execution platform. I strongly believe
that an automata based modeling and verification approach is more suited to easily describe any
potential scheduling system. Model checking techniques have been applied to the verification of
scheduling system. In these examples there have been a great degree of tailoring of the models to the
specific system [12, 3, 5].
Scientific Novelty: MULTI-CORE-SAFETY represents a novel composition of compositional
verification techniques and schedulability analysis. The potential for significantly influencing the
field of schedulability analysis is huge. In [13] experimental results are presented demonstrating that
for certain types of systems compositional model checking can be several orders of magnitude faster
than non-compositional verification. Compositional verification also has the advantage of leading to
2modular systems design and natural separation of concerns.
A lot of the research that is presented within the schedulability community lack real industrial
case-studies. En order to remedy this MULTI-CORE-SAFETY includes an industrial partner
which can provide such a case study and validate the relevance of the results.
Outcome of the Project More exact and scalable analysis for multi-core scheduling systems,
disseminated through publications and tools for schedulability analysis.
The Practical Feasibility of the Project: To ensure the relevance for the schedulability commu-
nity and an aligment with the most recent trends in the schedulability community, extensive coopera-
tion with the research group of Professor Insup Lee from the University of Pennsylvania will be part
of MULTI-CORE-SAFETY. The cooperation will be ensured through monthly video conferences,
yearly visits by researchers from University of Pennsylvania, and a three months external stay by
the PhD student. Insup Lee has worked extensively with certification of software for medical prod-
ucts under the US FDA (Food and Drug Administration). To ensure the relevance of the developed
schedulability tool as a vehicle for further research for other research groups, the project will also
include Axel Legay the leader of the ESTASYS (Efficient STAtistical methods in SYstems of Systems)
research team at INRIA Rennes.
To ensure the industrial relevance and applicability of the project, cooperation has been ensured
with the Danish industrial company Grundfos (www.grundfos.com). Grundfos Group has more than
18,000 employees worldwide and produces more than 16 million pump units per year. Their products
have a very long lifetime and thus need extremely high operating reliability. The main role of Grundfos
in the project is to provide a realistic case study.
The major part of the budget will provide funding for a PhD student, who together with the appli-
cant will be involved in all aspects of the project.
Hiring: The call for the PhD scholarship will be made together with a common call made by the de-
partment of computer science. The call will be widely advertised in the verification and schedulability
communities. The research unit has a history of attracting strong candidates.

Work Packages:

The research will be divided into three work packages.
WP1 – Modeling and semantics: Focusing on creating generic models needed for the automatic
translation and on defining a flexible specification language with a formal semantics.
WP2 – Tool development: Focusing a developing a robust tool implementation for the automatic
model translation and analysis using the back-end tool Ecdar.
WP3 – Evaluation: Focusing on evaluation of the developed tool on a realistic industrial case-study.

 

References

[1] Sebastian S. Bauer, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. A modal
specification theory for components with data. Sci. Comput. Program., 83:106–128, 2014.
[2] Gerd Behrmann, Alexandre David, and Kim Guldstrand Larsen. A tutorial on uppaal. In
Marco Bernardo and Flavio Corradini, editors, Formal Methods for the Design of Real-Time
Systems, International School on Formal Methods for the Design of Computer, Communica-
tion and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised
Lectures, volume 3185 of Lecture Notes in Computer Science, pages 200–236. Springer, 2004.
[3] Abdeldjalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim. G. Larsen, Marius Mikučionis,
Ulrik Nyman, and Arne Skou. Hierarchical scheduling framework based on compositional anal-
ysis using uppaal. In Proceedings of FACS 2013, lncs. Springer, 2013. To appear.
[4] Abdeldjalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim G. Larsen, Marius Mikucionis, Ul-
rik Nyman, and Arne Skou. Statistical and exact schedulability analysis of hierarchical schedul-
ing systems. Sci. Comput. Program., 127:103–130, 2016.
[5] Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Ulrik Nyman, Marius
Mikucionis, and Arne Skou. Widening the schedulability hierarchical scheduling systems. In
Proceedings of FACS 2014, 2014.
[6] Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Ulrik Nyman, and
Arne Skou. Schedulability and energy efficiency for multi-core hierarchical scheduling systems.
In Proceedings of ERTS2 2014, 2014.
[7] Jalil Boudjadar, Alexandre David, Jin Hyun Kim, Kim Guldstrand Larsen, Ulrik Nyman, Arne
Skou, and Marius Mikucionis. Degree of schedulability of mixed-criticality real-time systems
with probabilistic sporadic tasks. In Proceedings of TASE 2014, 2014.
[8] Jalil Boudjadar, Jin Hyun Kim, Kim Guldstrand Larsen, and Ulrik Nyman. Model checking
process algebra of communicating resources for real-time systems. In Proceedings of ECRTS
2014, 2014.
[9] Jalil Boudjadar, Kim Guldstrand Larsen, Jin Hyun Kim, and Ulrik Nyman. Compositional
schedulability analysis of an avionics system using uppaal. In ICAASE 2014, 2014.
[10] Laura Carnevali, Alessandro Pinzuti, and Enrico Vicario. Compositional verification for hierar-
chical scheduling of real-time systems. IEEE Transactions on Software Engineering, 39(5):638–
657, 2013.
[11] Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski. Timed I/O
automata: a complete specification theory for real-time systems. In Karl Henrik Johansson and
Wang Yi, editors, Proceedings of the 13th ACM International Conference on Hybrid Systems:
Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010, pages 91–100.
ACM, 2010.
[12] Alexandre David, Kim Guldstrand Larsen, Axel Legay, and Marius Mikučionis. Schedulability
of herschel-planck revisited using statistical model checking. In ISoLA (2), volume 7610 of
LNCS, pages 293–307. Springer, 2012.
[13] Alexandre David, Kim Guldstrand Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski.
ECDAR: an environment for compositional design and analysis of real time systems. In Ahmed
Bouajjani and Wei-Ngan Chin, editors, Automated Technology for Verification and Analysis
– 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings,
volume 6252 of Lecture Notes in Computer Science, pages 365–370. Springer, 2010.
[14] Robert I. Davis and Alan Burns. A survey of hard real-time scheduling for multiprocessor
systems. ACM Comput. Surv., 43(4):35:1–35:44, October 2011.
[15] Kim G. Larsen, Ulrik Nyman, and Andrzej W asowski. Interface input/output automata: Splitting
assumptions from guarantees. ENTCS. Elsevier Science Publishers, 2005.
[16] Kim Guldstrand Larsen, Ulrik Nyman, and Andrzej Wasowski. Interface input/output automata.
In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM, volume 4085 of Lecture
Notes in Computer Science, pages 82–97. Springer, 2006.
[17] Kim Guldstrand Larsen, Ulrik Nyman, and Andrzej W asowski. Modal i/o automata for interface
and product line theories. In Rocco De Nicola, editor, ESOP, volume 4421 of Lecture Notes in
Computer Science, pages 64–79. Springer, 2007.
[18] Kim Guldstrand Larsen, Ulrik Nyman, and Andrzej Wasowski.
On modal refinement and consistency. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR, volume 4703 of
Lecture Notes in Computer Science, pages 105–119. Springer, 2007.
[19] Safety Integrity Levels. https://en.wikipedia.org/wiki/safety_integrity_level.
[20] Insik Shin and Insup Lee. Periodic resource model for compositional real-time guarantees. In
RTSS, pages 2–13. IEEE Computer Society, 2003.
[21] Insik Shin and Insup Lee. Compositional real-time scheduling framework with periodic model.
ACM Trans. Embedded Comput. Syst., 7(3), 2008.
[22] Ecdar tool website. http://ecdar.cs.aau.dk.