Plenaries
Necmiye Ozay
University of Michigan
Formal methods for Cyber Physical Systems: State of the Art and Future Challenges
Modern cyber-physical systems, like high-end passenger vehicles, aircraft, or robots, are equipped with advanced sensing, learning, and decision making modules. On one hand these modules render the overall system more informed, possibly providing predictions into the future. On the other hand, they can be unreliable due to problems in information processing pipelines or decision making software. Formal methods, from verification and falsification to correct-by-construction synthesis hold the promise to detect and possibly eliminate such problems at design-time and to provide formal guarantees on systems’ correct operation. In this talk, I will discuss several recent advances in control synthesis and corner case generation for cyber-physical systems with a focus on scalability, and what role data and learning can play in this process. I will conclude the talk with some thoughts on challenges and interesting future directions.
Marcos V. Moreira
Federal University of Rio de Janeiro
Cryptographic systems and their applications in Discrete-Event Systems to ensure Confidentiality
One of the most critical issues related to the implementation of Cyber-Physical Systems (CPS) is information security, since one of the main features of this class of systems is the interconnection of its subsystems and components using communication networks, which makes CPS vulnerable to cyber-attacks. To ensure privacy and utility of the transmitted data, obfuscation strategies have been introduced in the literature, where the secret behavior must be hidden for the intruder while useful information must be recovered by the intended receiver. In this presentation, data confidentiality of CPS abstracted as Discrete-Event Systems is addressed, and the use of encipherment for ensuring privacy and utility is discussed.
Laurent Hardouin
University of Angers
On Counter Functions and Operators for Modelling Discrete-Event Dynamic Systems.
To ensure control of discrete-event dynamic systems, it is common to timestamp the occurrence of events to capture their dynamics, or alternatively, it is interesting to count the number of occurrences of these events. This second point of view leads to defining non-continuous functions called “counters” that are monotonically non-decreasing. They allow describing the temporal evolution of observed events. The non-decreasing nature of these signals naturally leads to studying them in an idempotent semiring.
