Séminaire du 15 juin 2018


LIPN, CNRS UMR 7030, Université Paris 13, Institut Galilée, salle B107.


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.

15h30-16h00: pause café

16h00-17h00: vie du groupe