Chair ASC production

The Chair is structured around four teams across four schools, each focusing on distinct yet complementary fields of teaching and research

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 

More than 10 exchange and dialogue procedures are currently underway, aimed at validating the opportunity to launch specific research projects involving industrial partners, government stakeholders, and the four participating schools. (Details not disclosable)

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 

Two CIEDS projects in the fields of robotics and modeling currently involve the stakeholders of the ASC Chair." (Details not disclosable)

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 

Correct-by-construction requirement decomposition

Georgios BAKIRTZIS

Correct-by-construction requirement decomposition / Décomposition des exigences correcte par construction

In systems engineering, accurately decomposing requirements is crucial for creating well-defined and manageable system components, particularly in safety-critical domains. Despite the critical need, rigorous, top-down methodologies for effectively breaking down complex requirements into precise, actionable sub-requirements are scarce, especially compared to the wealth of bottom-up verification techniques. Addressing this gap, we introduce a formal decomposition for contract-based design that guarantees the correctness of decomposed requirements if specific conditions are met. Our (semi-)automated methodology augments contract-based design with reachability analysis and constraint programming to systematically identify, verify, and validate sub-requirements representable by continuous bounded sets---continuous relations between real-valued inputs and outputs. We demonstrate the efficacy and practicality of a correct-by-construction approach through a comprehensive case study on a cruise control system, highlighting how our methodology improves the interpretability, tractability, and verifiability of system requirements. 

More informations : 

• Lien vers l'article
• Lien vers le post LinkedIn associé

Safety Assurance under Uncertainties From Software to Cyber-Physical/Machine Learning Systems

Jérémy DUBUT

Ensuring the safety of software systems has never been as pressing an issue as it is today. Practitioners and researchers addressing this challenge face a unique problem inherent to modern software systems: uncertainty. On the one hand, the cyber-physical nature of modern software systems—exemplified by automated driving systems—requires addressing environmental uncertainties and mitigating the associated risks. Additionally, the proliferation of statistical machine learning components and massive numerical computation units for statistical reasoning, such as deep neural networks, makes these systems difficult to explain, understand, analyze, or verify.

This book is the first to provide a comprehensive overview of these unified and interdisciplinary efforts. Using automated driving systems as a primary example, it describes various techniques for specifying, modeling, testing, analyzing, and verifying modern software systems.

In his field of expertise, Jérémy Dubut-Kross co-authored the chapter "Formal Specification of Temporal Properties," which serves as a foundation for many other chapters in the book. This chapter introduces what are known as formal specifications. Formal specifications are essential whenever one seeks to automatically verify whether a system behaves as expected for a given input. They are therefore indispensable in numerous testing and verification methods.

"Safety Assurance under Uncertainties" is thus a seminal work that belongs in the libraries of all organizations involved in the validation of critical systems.

More informations :

• Lien vers l'article
• Lien vers le post LinkedIn associé

Petri Nets and Higher-Dimensional Automata

Philipp SCHLEHUBER

Petri Nets as Higher-Dimensional Automata Petri nets and their variants are often studied through their interleaving semantics, that is, by considering executions where only one transition occurs at each step. This clearly represents a limitation, as Petri nets are inherently a model of true concurrency. This paper revisits the semantics of Petri nets as higher-dimensional automata (HDAs), as introduced by van Glabbeek, which systematically account for concurrency.

The authors extend the translation to include common features. They consider nets with inhibitor arcs under the two concurrent semantics used in the literature, as well as generalized self-modifying nets. Finally, the authors present a tool implementing their translations.

More informations :

• Lien vers l'article
• Lien vers le post LinkedIn associé

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .