Due to the critical consequences of possible failures, robot systems must be formally verified to guarantee that their behaviors are correct and safe. There is, however, a gap in terms of building safe behaviors between the formal methods and robotic communities as the latter focuses on informal design and its implementation in a manner which is accessible to robotics engineers. In this paper, we present an approach to bridge that gap which enables a tight coupling of informal robot behaviors defined in SMACH, Python state machine API, with formal models through a process of translation. A set of mapping rules, which facilitates transformation is provided and the result is utilized for formal verification of safety properties. We also discuss the current limitations of such work along with recommendations on how these might be addressed.

This paper introduces an approach for translating Behaviour-Driven Development (BDD) scenarios written under a domain-specific language (DSL) into Timed Automata (TA) to al-low for formal verification of real-time systems. A set of mapping rules is presented to facilitate the translation. We demonstrate the feasibility of our approach through an illustrative example of a vending machine that operates under a particular set of time constraints. Our proof-of-concept indicates that this approach is an important step towards ensuring compatibility between high-level software specifications (BDD scenarios) and formal models (TA models). We also discuss the current limitations of such work along with recommendations on how these might be addressed.

Modeling and analysis of timing constraints is crucial in real-time automotive systems. Modern vehicles are interconnected through wireless networks which creates vulnerabilities to external malicious attacks. Violations of cyber-security can cause safety related accidents and serious damages. To identify the potential impacts of security related threats on safety properties of interconnected automotive systems, this paper presents analysis techniques that support verification and validation (V&V) of safety & security (S/S) related timing constraints on those systems: Probabilistic extension of S/S timing constraints are specified in Pr Ccsl (probabilistic extension of clock constraint specification language) and the semantics of the extended constraints are translated into verifiable Uppaal models with stochastic semantics for formal verification. A set of mapping rules are proposed to facilitate the translation. An automatic translation tool, namely ProTL, is implemented based on the mapping rules. Formal verification are performed on the S/S timing constraints using Uppaal-SMC under different attack scenarios. Our approach is demonstrated on a cooperative automotive system case study.

Formal analysis of functional and non-functional requirements is crucial in automotive systems. The behaviors of those systems often rely on complex dynamics as well as on stochastic behaviors. We have proposed a probabilistic extension of Clock Constraint Specification Language, called PrCCSL, for specification of (non)-functional requirements and proved the correctness of requirements by mapping the semantics of the specifications into UPPAAL models. Previous work is extended in this paper by including an extension of PrCCSL, called PrCCSL*, for specification of stochastic and dynamic system behaviors, as well as complex requirements related to multiple events. To formally analyze the system behaviors/requirements specified in PrCCSL*, the PrCCSL* specifications are translated into stochastic UPPAAL models for formal verification. We implement an automatic translation tool, namely ProTL, which can also perform formal analysis on PrCCSL* specifications using UPPAAL-SMC as an analysis backend. Our approach is demonstrated on two automotive systems case studies.

Formal analysis of functional and non-functional requirements is crucial in cyber-physical systems (CPS), in which controllers interact with physical environments. The continuous time behaviors of CPS often rely on complex dynamics as well as on stochastic behaviors. We have previously proposed a probabilistic extension of Clock Constraint Specification Language, called PrCCSL, for specification of (non)-functional requirements of CPS and proved the correctness of requirements by mapping the semantics of the specifications into verifiable UPPAAL models. Previous work is extended in this paper by including an extension of PrCCSL, i.e., PrCCSL*, which incorporates annotations of continuous behaviors and stochastic characteristics of CPS. The CPS behaviors are specified in PrCCSL* and translated into stochastic UPPAAL models for formal verification. The translation algorithm from PrCCSL* into UPPAAL models is provided and implemented in an automatic translation tool, namely ProTL. Formal verification of CPS against (non)-functional requirements is performed by ProTL using UPPAAL-SMC as an analysis backend. Our approach is demonstrated on a series of CPS case studies.

Ensuring correctness of timed behaviors in cyber-physical systems (CPS) using closed-loop verification is challenging due to the hybrid dynamics in both systems and environments. Simulink and Stateflow are tools for model-based design that support a variety of mechanisms for modeling and analyzing hybrid dynamics of real-time embedded systems. In this paper, we present an SMT-based approach for formal analysis of the hybrid-dynamic timing behaviors of CPS modeled in Simulink blocks and Stateflow states (S/S). The hierarchically interconnected S/S are flattened and translated into the input language of SMT solver for formal verification. A translation algorithm is provided to facilitate the translation. Formal verification of timing constraints against the S/S models is reduced to the validity checking of the resulting SMT encodings. The applicability of our approach is demonstrated on an unmanned surface vessel case study.

EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design. We have previously developed a translator, called A-BeTA, transforming timed behavioral constraints in EAST-ADL into the analyzable UPPAAL models. In this paper, we extend the previous work by including support for Stateflow, which is used to design event-driven systems via hierarchical state machines and flow charts. However, Stateflow provides limited support for formal analysis and often suffers from incomplete coverage issues since it was originally designed for the simulation of designs and as such does not provide a model amenable to formal verification. We tackle that shortcoming by transforming Stateflow models into verifiable UPPAAL models and integrating the translation with formal analysis techniques: a flattening strategy is proposed to facilitate the guarantee of translation. Furthermore, a set of mapping rules is presented to ensure the translation is correct, efficient, and applicable to real case studies. The analysis techniques, including the flattening and mapping strategy, are validated and demonstrated on two automotive case studies.

EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design with a focus on structural specification and behavioral constraints. The current concept of EAST-ADL provides limited support for modeling and analysis of Energy-aware Real-Time (ERT) behaviors due to the absence of energy constraints modeling notations and the lack of formal semantics. We address these limitations by extending the EAST-ADL notation with energy constraints and integrating this extension with formal modeling and analysis techniques. We provide a mapping scheme as the basis for automatic model transformation between the extended EAST-ADL and priced timed automata for model checking. This methodology has been implemented in a tool called A-BeTA and is demonstrated by means of the Brake-By-Wire case study. Our approach enables formal modeling and verification of ERT systems in EAST-ADL and identifies potential conflicts between different automotive functions at an early stage of development.

Software-Defined Networking (SDN) is a network architecture where a controller manages flow control to enable intelligent networking. Currently, a popular specification for creating an SDN is an open standard called OpenFlow. The behavior of the SDN OpenFlow (SDN-OF) is critical to the safety of the network system and its correctness must be proven so as to avoid system failures. In this paper, we report our experience in applying formal techniques for modeling and analysis of SDN-OF. The formal model of SDN-OF is described in detail and its correctness is formalized in logical formulas based on the informal specification. The desired properties are verified over the model using VERSA and UPPAAL. Our work-in-progressinvolves the development of a model translation tool that facilitates automatic conversion of the verified model to Python for modular code synthesis on the application platform

Abstract This article discusses a new format of predicate diagrams for the verification of real-time systems. We consider systems that are defined as extended timed graphs, a format that combines timed automata and constructs for modelling data, possibly over infinite domains. Predicate diagrams are succinct and intuitive representations of Boolean abstractions. They also represent an interface between deductive tools used to establish the correctness of an abstraction, and model checking tools that can verify behavioral properties of finite-state models. The contribution of this article is to extend the format of predicate diagrams to timed systems. We establish a set of verification conditions that are sufficient to prove that a given predicate diagram is a correct abstraction of an extended timed graph; these verification conditions can often be discharged with SMT solvers such as CVC-lite. Additionally, we describe how this approach extends naturally to the verification of parameterized systems. The formalism is supported by a toolkit, and we demonstrate its use at the hand of Fischer’s real-time mutual-exclusion protocol.

My research area is fundamental of formal analysis of real-time embedded systems. The main objective of this research is the theoretical and practical development of a verification algorithm for the formal analysis of real-time embedded systems based on the combination of real-time model checking and abstract interpretation of real-time models. The objective of the proposed combination is an improved behavior both in time and space requirement of the resulting algorithm. One of drawbacks of all current real-time model-checking tools is the limited size of the systems that can be analyzed. By combination of state-space exploration with abstract interpretation we expect to scale up the size of applications.