%0 Conference Proceedings
%T Model Checking of SCADE Designed Systems
%+ Communication & Systèmes [Toulouse] (C-S)
%+ Lab-STICC_ENSTAB_CACS_MOCS
%+ Pôle STIC_IDM
%A Heim, S
%A Dumas, Xavier
%A Bonnafous, E
%A Dhaussy, Philippe
%A Teodorov, C
%A Leroux, Lise
%< avec comité de lecture
%( Proceedings of the 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016)
%B 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016)
%C TOULOUSE, France
%8 2016-01-27
%D 2016
%K model checking
%K formal methods
%K CDL
%K SCADE
%K LUSTRE
%K OBP
%K synchronous
%K asynchronous
%Z Computer Science [cs]/Embedded SystemsConference papers
%X Model checking is a well-known method to verify a formal model in all possible configurations. Nevertheless this technique can hardly scale up to industrial asynchronous systems because of the state-space explosion problem. To address this challenge, a new approach based on context specification (the environment of the system) and an observation engine called OBP (Observer Based Prover) has been developed. The idea is that given a property to be verified, one doesn’t need to explore all possible configurations of the complete system. Among all possible behavior of the system, a tiny part is representative enough for the property to be verified. Thus, specifying a pertinent environment (a context) allows restricting the system behavior on those only parts where the property is worth verifying.The objective of our work is to apply this Context-aware verification method to the verification of SCADE systems designed in LUSTRE language, in order to check behavioral properties related to system safety. Moreover LUSTRE is a synchronous language whereas OBP exploration engine takes as input an asynchronous model designed in FIACRE language. To cope with this problem our approach consists in developing a GALS method combining asynchronous contexts with synchronous models.
%G English
%2 https://hal.science/hal-01289454/document
%2 https://hal.science/hal-01289454/file/paper_9.pdf
%L hal-01289454
%U https://hal.science/hal-01289454
%~ UNIV-BREST
%~ INSTITUT-TELECOM
%~ ENSTA-BRETAGNE
%~ CNRS
%~ UNIV-UBS
%~ ENSTA-BRETAGNE-STIC
%~ LAB-STICC
%~ ERTS2016
%~ INSTITUTS-TELECOM