Séminaires
Séminaire du 15 juin 2018
Lieu
LIPN, CNRS UMR 7030, Université Paris 13, Institut Galilée, salle B107.
Programme
14h00-15h00: Wojtek Jamroga (Polish Academy of Sciences) Model Checking Strategic Ability: Why, What, and Especially: How?
Abstract : 
Automated verification of discrete-state systems has been a hot topic in
computer science for over 35 years. Model checking of temporal and
strategic properties is one of the most prominent and most successful
approaches here. I will present a brief introduction to the topic, and
mention some relevant properties that one might like to verify this way.
Then, I will talk about some recent results on approximate model
checking and model reductions, which can be applied to facilitate
verification of notoriously hard cases.
15h00-15h30 : Yan Duplouy (LSV, IRT SystemX ) Integrating Simulink Models into the Model Checker Cosmos
Abstract : -->
The validation of safety properties is a crucial concern
for the design of computer guided systems, in particular for
cyber-physical systems. For instance, in transport systems, a classical
approach consists in analyzing the interactions of a randomized
environment (roads, cross-sections, etc.) with a vehicle controller,
often derived from a Simulink model. However, while largely used in
practice by industrial system designers, Simulink does not benefit from
a formal semantics. Thus engineers usually have to infer the behaviours
of their models from experiments which weakens the validation process.
For this reason, several works proposed formal translations from
(subsets of) Simulink blocks to other models like hybrid automata [1,2],
or languages like Lustre [3]. Other works directly define exact
semantics [4] or operational semantics [5] for Simulink. We follow the
latter approach and propose semantics for a significant fragment of
Simulink. We proceed in two steps: we first develop an exact version,
and then enrich it with effective procedures that were integrated into
the statistical model checker Cosmos. With the resulting tool, we obtain
performance indices for models combining a randomized environment
described by a stochastic Petri net and a controller described in
Simulink, as illustrated for a double heater system.
[1] Tiwari, A.: Formal Semantics and Analysis methods for Simulink Stateflow Models. Tech. rep.
[2] Agrawal, A., Simon, G., Karsai, G.: Semantic Translation of Simulink/Stateflow Models to Hybrid Automata Using Graph Transformations. Electr. Notes Theor. Comput. Sci.
[3] Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embedded Comput. Syst.
[4] Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybrid systems modelers. Journal of Computer and System Sciences
[5] Bouissou, O., Chapoutot, A.: An operational semantics for simulink's simulation engine. In: Proceedings of the 13th ACM SIGPLAN/SIGBED.