3^rd Workshop on Formal Verification of Physical Systems (FVPS 2024)

Programme, Monday, August 5, 2024

Theme

One of the main issues behind many failing systems is the ad-hoc verification approach that involves a variety of formalism and techniques for the modeling and analysis of various components of the present-age (cyber)-physical systems. For example, control and communication protocols are usually modeled using automata theory, and thus analyzed using model checking techniques, while the modeling of physical aspects often requires multivariate calculus foundations, which are in turn analyzed using paper-and-pencil based analytical proofs, simulation or theorem proving. The fundamental differences between these modeling and analysis techniques limit us to analyze the whole system as one unit and thus miss many corner cases, which arise due to the operation of all the sub-components of the system together. One of the major concerns is that, despite the above-mentioned evident limitation in the analysis methods, many safety-critical systems, such as aerospace, smart-transportation, smart-grid and e-healthcare, are increasingly involving physical elements. Moreover, we are moving towards integrating more complex physical elements in our engineering systems. For example, we are looking into developing Quantum Computers to meet high performance needs. Similarly, photonic components are increasingly being advocated and used in aerospace applications due to their lightweight and temperature independency compared to traditional electronics based components. Finally, the impact of physical components is relevant to both safety and security of the overall system. For example, malfunction in sensor measurement may lead to safety issues whereas sophisticated physics based side-channel (e.g., power and acoustic measurements) attacks lead to the security violation of the underlying system.

The focus of the workshop will be on formal verification techniques and for the modeling, analysis and verification of safety and security critical physical systems. We encourage submissions on interdisciplinary approaches that bring together formal methods and techniques from other knowledge areas such as quantum computing, control theory, biology, optimization theory and artificial intelligence.

Topics of Interest

General Topics
• Formalization of physic’s mathematics and theories
• Interactive and automated theorem proving for physical systems
• Model Checking algorithms and tools for physical systems
• Formalization of security and safety of physical systems
• Runtime verification of safety and security properties
• Combination of formal, semiformal and infromal approaches
• Formal verification of numerical algorithms
• Refinement based verification of physical systems
• Formalization of probability, reliability and statistical metrics
• Hybrid systems for physical systems modeling and verification
• Benchmarks for physical systems
• Formal requirement specification and validation

Application Domains
• Aerospace and avionics systems
• Automotive cyber physical systems
• Autonomous vehicles
• Robotics
• Smartgrids
• Smart transportation
• Human factor modeling and analysis
• Biological and healthcare systems

Formal model engineering--where tools used by model developers are equipped with automatic formal analysis methods--is a promising way to integrate formal methods into model development. However, supporting formal model engineering for cyber-physical systems (CPSs) introduces several challenges, including: (i) the high expressiveness of industrial modeling languages, (ii) the difficulty of exhaustive model checking analysis due to asynchronous behaviors, and (iii) the complex interactions between advanced control programs and physical environments typical of many CPSs. This talk outlines our approach to support efficient formal model engineering for synchronous CPS designs with physical environments in the avionics modeling standard AADL and its OSATE tool environment. For this purpose, we have identified a suitable sublanguage of AADL, called Synchronous AADL, in which the synchronous designs of CPSs, including those with physical environments, can be specified naturally in AADL. We have defined the formal semantics of Synchronous AADL in rewriting logic, and integrated automatic formal analysis of Synchronous AADL models via Maude and SMT solving into OSATE. Our approach addresses the above challenges by: (i) leveraging the expressive power of Maude for complex control programs; (ii) developing automatic formal analysis methods for synchronous designs; and (iii) integrating Maude and SMT solving to analyze interactions between control programs and physical environments. We also show how synchronizers, such as PALS, TTA, and MSYNC, can verify the correctness of distributed CPS implementations based on their synchronous designs. We summarize our experiences on applications such as industrial avionics control systems, airplane turning algorithms, and collaborating drones.

The advent of automotive cyber-physical systems (CPS) has significantly enhanced vehicular safety, efficiency, and user experience. However, the increasing complexity and interconnectedness of these systems introduce substantial risks related to reliability, security, and correctness. Formal methods, which involve mathematically rigorous techniques for specification, development, and verification of software and hardware, are crucial in addressing these challenges. By employing formal methods, automotive CPS can be rigorously tested and verified, ensuring robust performance, mitigating risks, and paving the way for safer and more reliable automotive technologies. This talk will explore the functional safety aspects of automotive CPS particularly due to software, the standardization of software development, and some industrial use cases of formal methods in verifying complex software. The talk will briefly present a case study where the bug prediction model estimates that the use of formal verification reduced the number of residual bugs. The field monitoring validated the bug prediction model estimates. Lastly, the talk will highlight the challenges of using formal methods in the software industry.

As cryptographic systems grow increasingly complex and vital to our digital infrastructure, the need for rigorous verification methods has become critical. Traditional security analysis approaches often fail to identify subtle vulnerabilities, particularly those exploited through side-channel attacks. This paper outlines the current state of formal verification in cryptography, focusing on the challenges in formally analyzing side-channel attacks. It also proposes future research directions in this crucial area, aiming to enhance the security and reliability of cryptographic implementations.

Hybrid programs are modeling artifacts for complex physical systems that involve discrete and con- tinuous behaviors. Plaidypvs is an implementation of differential dynamic logic (dL) in the Prototype Verification System (PVS) that allows for the specification and formalized reasoning of hybrid programs. Profiting from the higher-order logic provided by PVS, Plaidypvs enables the specification and verification of hybrid program schemas. A hybrid program schema represents a family of programs, such as programs with an arbitrary number of variables. This is particularly useful when analyzing hybrid systems where the number of actors is unknown, for example, when studying the behavior of vehicles following a merging protocol as they pass through an intersection. The formal reasoning of such hybrid programs, for a known number of vehicles, is doable in dL, but the complexity of the proof increases with the number of vehicles. The formal reasoning of hybrid programs for an arbitrary but unknown number of vehicles falls beyond the scope of the rules of dL. This paper presents a formal verification in Plaidypvs of a merging protocol through an intersection with arbitrarily many vehicles. The verification proves an invariant safety property of this system, namely that loss of separation is never achieved when obeying the merging protocol. This invariant property is encoded as a deductive rule in Plaidypvs. This work serves as a proof of concept towards a logic that allows for reasoning of hybrid program schemas modeling systems with an unknown number of actors.

Submission

• Abstract (upto 2 pages)
• Regular papers (upto 6 pages)

Journal Special Issue

Important Dates

• Full Paper Submission: Continuous submission until July 12, 2024 (Early submission leads to early notification)
• Camera Ready: July 26, 2024
• Workshop: August 5, 2024

Program Chairs

• Adnan Rashid, Concordia University, Montreal, QC, Canada
• Osman Hasan, National University of Sciences and Technology (NUST), Pakistan
• Sofiene Tahar , Concordia University, Montreal, QC, Canada

Program Committee

• Aaron Dutle, NASA, USA
• Atif Mashkoor, Institute for Software Systems Engineering, Johannes Kepler University, Linz, Austria
• Pedro Ribeiro, University of York, UK
• Peter Csaba Ölveczky, University of Oslo, Norway
• Waqar Ahmed, Wind River, Canada