We propose a new deductive model checking methodology where narrowing-based logical model checking of symbolic states specified as disjunctions of constrained patterns is combined with inductive theorem proving to discharge inductive verification conditions that ensure useful symbolic state space reductions. An obvious combination is to use an inductive theorem prover in automated mode as an oracle to help logical model checking reach a fixpoint. But this is not the only possible combination. In this paper we focus instead on a new deductive model checking methodology to verify invariants —including inductive invariants— of infinite-state systems, where logical model checking automates large parts of the verification effort with the help of an inductive theorem prover as an oracle . Inductive verification conditions not discharged automatically by the oracle are dealt with by commands that refine some constrained patterns by useful semantic equivalences, and by using an inductive theorem prover in interactive mode. This methodology is demonstrated by means of concurrent system examples using two Maude tools working in tandem: the DM-Check narrowing-based symbolic model checker, and the NuITP inductive theorem prover.

Many cyber-physical systems (CPSs) consist of a collection of components with both continuous environments and advanced control programs. Many such CPSs are either synchronous , in which the components operate in lockstep, or virtually synchronous , where the “underlying design” is synchronous but the system itself is asynchronous since it is a distributed system. A CPS may involve different kinds or brands of components, which may therefore operate with different frequencies. In addition, each component may be composed of multiple subsystems with different frequencies. This paper presents the MR-HybridSynchAADL modeling language and verification tool for modeling and analyzing the synchronous designs of synchronous and virtually synchronous hierarchical multirate CPSs with advanced control programs, continuous behaviors, and imprecise local clocks. For virtually synchronous CPSs, the Hybrid PALS synchronizer implies that verifying the much simpler underlying synchronous design also verifies the corresponding distributed system. We define both a symbolic semantics for the synchronous composition of the components, capturing continuous behaviors and timing uncertainties, and a concrete semantics, for simulation, in rewriting logic, in a modular way to ensure consistency between these two semantics. MR-HybridSynchAADL provides randomized simulation and Maude-with-SMT-based reachability analysis, and is fully integrated into the OSATE tool environment for the avionics modeling standard AADL. We illustrate the use of MR-HybridSynchAADL on a collection of UAVs with different frequencies that deliver packets and adapt to their dynamically changing environments to avoid collisions.

Abstract Trusted execution environments (TEEs) have emerged as a key technology in the cybersecurity domain. A TEE provides an isolated environment in which sensitive computations can be executed securely. Trusted applications running in TEEs are developed using standardized APIs that many hardware platforms for TEE adhere to. However, formal models tailored to standard TEE APIs are not well developed. In this paper, we present a formal specification of TEE APIs using Maude. We focus on Trusted Storage API and Cryptographic Operations API, which are foundational to mobile and IoT applications. The effectiveness of our approach is demonstrated through formal analysis of MQT-TZ, an open-source TEE application for IoT. Our formal analysis has revealed security vulnerabilities in the implementation of MQT-TZ, and we patch and confirm its integrity using model checking.

Abstract Programmable logic controllers (PLCs) are widely used in industrial applications. Ensuring the correctness of PLC programs is important due to their safety-critical nature. Structured text (ST) is an imperative programming language for PLC. Despite recent advances in executable semantics of PLC ST, existing methods neglect complex multitasking and preemption features. This paper presents an executable semantics of PLC ST with preemptive multitasking. Formal analysis of multitasking programs experiences the state explosion problem. To mitigate this problem, this paper also proposes state space reduction techniques for model checking multitask PLC ST programs.

This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the “standard” semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude—including full LTL model checking, analysis with user-defined execution strategies, and even statistical model checking—for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Roméo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Roméo in many cases.

Abstract We present theSTLmcmodel checker for signal temporal logic (STL) properties of hybrid systems. TheSTLmctool can perform STL model checking up to a robustness threshold for a wide range of hybrid systems. Our tool utilizes the refutation-complete SMT-based bounded model checking algorithm by reducing the robust STL model checking problem into Boolean STL model checking. IfSTLmcdoes not find a counterexample, the system is guaranteed to be correct up to the given bounds and robustness threshold. We demonstrate the effectiveness ofSTLmcon a number of hybrid system benchmarks.

Abstract We present the $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ H Y B R I D S Y N C H AADL modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, bounded clock skews, network delays, and execution times. We leverage the Hybrid PALS equivalence, so that it is sufficient to model and verify the simpler underlying synchronous designs. We define the $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ H Y B R I D S Y N C H AADL language as a sublanguage of the avionics modeling standard AADL for modeling such designs in AADL, and demonstrate the effectiveness of $$\textsc {Hybrid}\textsc {Synch}\textsc {AADL}$$ H Y B R I D S Y N C H AADL on a number of applications.

Signal temporal logic (STL) is widely used to specify and analyze properties of cyber-physical systems with continuous behaviors. However, STL model checking is still quite limited, as existing STL model checking methods are either incomplete or very inefficient. This paper presents a new SMT-based model checking algorithm for verifying STL properties of cyber-physical systems. We propose a novel translation technique to reduce the STL bounded model checking problem to the satisfiability of a first-order logic formula over reals, which can be solved using state-of-the-art SMT solvers. Our algorithm is based on a new theoretical result, presented in this paper, to build a small but complete discretization of continuous signals, which preserves the bounded satisfiability of STL. Our translation method allows an efficient STL model checking algorithm that is refutationally complete for bounded signals, and that is much more scalable than the previous refutationally complete algorithm.

TTA and PALS are two prominent formal design patterns—with different strengths and weaknesses—for virtually synchronous distributed cyber-physical systems (CPSs). They greatly simplify the design and verification of such systems by allowing us to design and verify their underlying synchronous designs. In this paper we introduce and verify MSYNC as a formal design (and verification) pattern/synchronizer for hierarchical multirate CPSs that generalizes, and combines the advantages of, both TTA and (single-rate and multirate) PALS. We also define an extension of TTA to multirate CPSs as a special case. We show that MSYNC outperforms both TTA and PALS in terms of allowing shorter periods, and illustrate the MSYNC design and verification approach with a case study on a fault-tolerant distributed control system for turning an airplane.

Signal temporal logic (STL) is a temporal logic formalism for specifying properties of continuous signals. STL is widely used for analyzing programs in cyber-physical systems (CPS) that interact with physical entities. However, existing methods for analyzing STL properties are incomplete even for bounded signals, and thus cannot guarantee the correctness of CPS programs. This paper presents a new symbolic model checking algorithm for CPS programs that is refutationally complete for general STL properties of bounded signals. To address the difficulties of dealing with an infinite state space over a continuous time domain, we first propose a syntactic separation of STL, which decomposes an STL formula into an equivalent formula so that each subformula depends only on one of the disjoint segments of a signal. Using the syntactic separation, an STL model checking problem can be reduced to the satisfiability of a first-order logic formula, which is decidable for CPS programs with polynomial dynamics using satisfiability modulo theories (SMT). Unlike the previous methods, our method can verify the correctness of CPS programs for STL properties up to given bounds.

We present SMT-based techniques for analyzing networks of nonlinear hybrid systems, which interact with each other in both discrete and continuous ways. We propose a modular encoding method to reduce reachability problems of hybrid components, involving continuous I/O as well as usual discrete I/O, into the satisfiability of first-order logic formulas over the real numbers. We identify a generic class of logical formulas to modularly encode networks of hybrid systems, and present an SMT algorithm for checking the satisfiability of such logical formulas. The experimental results show that our techniques significantly increase the performance of SMT-based analysis for networks of nonlinear hybrid components.

This paper presents general techniques for verifying virtually synchronous distributed control systems with interconnected physical environments. Such cyber-physical systems (CPSs) are notoriously hard to verify, due to their combination of nontrivial continuous dynamics, network delays, imprecise local clocks, asynchronous communication, etc. To simplify their analysis, we first extend the PALS methodology---that allows to abstract from the timing of events, asynchronous communication, network delays, and imprecise clocks, as long as the infrastructure guarantees bounds on the network delays and clock skews---from real-time to hybrid systems. We prove a bisimulation equivalence between Hybrid PALS synchronous and asynchronous models. We then show how various verification problems for synchronous Hybrid PALS models can be reduced to SMT solving over nonlinear theories of the real numbers. We illustrate the Hybrid PALS modeling and verification methodology on a number of CPSs, including a control system for turning an airplane.

High level Petri nets (HLPNs) have been widely applied to model concurrent and distributed systems in computer science and many other engineering disciplines. However, due to the expressive power of HLPNs, they are difficult to analyze. In recent years, a variety of new analysis techniques based on model checking have been proposed to analyze high level Petri nets in addition to the traditional analysis techniques such as simulation and reachability (coverability) tree. These new analysis techniques include (1) developing tailored model checkers for particular types of HLPNs or (2) leveraging existing general model checkers through model translation where a HLPN is transformed into an equivalent form suitable for the target model checker. In this paper, we present a term rewriting approach to analyze a particular type of HLPNs -- predicate transition nets (PrT nets). Our approach is completely automatic and implemented in our tool environment, where the frontend is PIPE+, a general graphical editor for creating PrT net models, and the backend is Maude, a well-known term rewriting system. We have applied our approach to the Mondex system -- the 1st pilot project of verified software repository in the worldwide software verification grand challenge, and several well-known problems used in the annual model checking contest of Petri net tools. Our initial experimental results are encouraging and demonstrate the usefulness of the approach.

A concurrent system can be naturally specified as a rewrite theory R = (Sigma, E, R) where states are elements of the initial algebra of terms modulo E and concurrent transitions are axiomatized by the rewrite rules R. Under simple conditions, narrowing with rules R modulo equations E can be used to symbolically represent the system's state space by means of terms with logical variables. We call this symbolic representation a "logical state space" and it can also be used for model checking verification of LTL properties. Since in general such a logical state space can be infinite, we propose several abstraction techniques for obtaining either an over-approximation or an under-approximation of the logical state space: (i) a folding abstraction that collapses patterns into more general ones, (ii) an easy-to-check method to define (bisimilar) equational abstractions, and (iii) an iterated bounded model checking method that can detect if a logical state space within a given bound is complete. We also show that folding abstractions can be faithful for safety LTL properties, so that they do not generate any spurious counterexamples. These abstraction methods can be used in combination and, as we illustrate with examples, can be effective in making the logical state space finite. We have implemented these techniques in the Maude system, providing the first narrowing-based LTL model checker we are aware of.