LIPN, CNRS UMR 7030, Université Paris 13, Institut Galilée, salle B107.
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.
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 . Other works directly define exact
semantics  or operational semantics  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.
 Tiwari, A.: Formal Semantics and Analysis methods for Simulink Stateflow Models. Tech. rep.
 Agrawal, A., Simon, G., Karsai, G.: Semantic Translation of Simulink/Stateflow Models to Hybrid Automata Using Graph Transformations. Electr. Notes Theor. Comput. Sci.
 Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embedded Comput. Syst.
 Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybrid systems modelers. Journal of Computer and System Sciences
 Bouissou, O., Chapoutot, A.: An operational semantics for simulink's simulation engine. In: Proceedings of the 13th ACM SIGPLAN/SIGBED.