Modular SMT-Based Analysis of Nonlinear Hybrid Systems.
Kyungmin Bae and Sicun Gao.
International Conference on Formal Methods in Computer-Aided Design (FMCAD 2017), to appear.
Rewriting modulo SMT is a novel symbolic technique to model and analyze infinite-state systems that interact with a nondeterministic environment. It seamlessly combines rewriting modulo equational theories, SMT solving, and model checking. One of the main challenges of this technique is to cope with the symbolic state-space explosion problem. This paper presents guarded terms, an approach to deal with this problem for rewriting modulo SMT. Guarded terms can encode many symbolic states into one by using SMT constraints as part of the term structure. This approach enables the reduction of the symbolic state space by limiting branching due to concurrent computation, and the complexity and size of constraints by distributing them in the term structure. A case study of an unbounded and symbolic priority queue illustrates the approach.
- SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems.
Kyungmin Bae, Peter Ölveczky, Soonho Kong, Sicun Gao, and Edmund M. Clarke.
ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2016).
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.
A Hybrid Architecture for Correct-by-Construction Hybrid Planning and Control.
Robert P. Goldman, Daniel Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae.
International Symposium on NASA Formal Methods (NFM 2016).
[abstract] [link]This paper describes Hy-CIRCA, an architecture for verified, correct-by-construction planning and execution for hybrid systems, including nonlinear continuous dynamics. Hy-CIRCA addresses the high computational complexity of such systems by first planning at an abstract level, and then progressively refining the original plan. Hy-CIRCA integrates the dReal nonlinear SMT solver with enhanced versions of the SHOP2 HTN planner and the CIRCA Controller Synthesis Module (CSM). SHOP2 computes a high level nominal mission plan, the CIRCA CSM develops reactive controllers for the mission steps, accounting for disturbances, and dReal verifies that the plans are correct with respect to continuous dynamics. In this way, Hy-CIRCA decomposes reasoning about the plan and judiciously applies the different solvers to the problems they are best at.
An Architecture for Hybrid Planning and Execution.
Robert P. Goldman, Dan Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae.
AAAI-16 Workshop on Planning for Hybrid Systems (PlanHS 2016).
[abstract] [link]This paper describes Hy-CIRCA, an architecture for verified, correct-by-construction planning and execution for hybrid systems, including non-linear continuous dynamics. Hy-CIRCA addresses the high computational complexity of such systems by first planning at an abstract level, and then progressively refining the original plan. Hy-CIRCA is an extension of our Playbook approach, which aims to make it easy for users to exert supervisory control over multiple autonomous systems by “calling a play.” The Playbook approach is implemented by combining (1) a human-machine interface for commanding and monitoring the autonomous systems; (2) a hierarchical planner for translating commands into executable plans; and (3) a smart executive to manage plan execution by coordinating the control systems of the individual autonomous agents, tracking plan execution, and triggering replanning when necessary. Hy-CIRCA integrates the dReal non-linear SMT solver, with enhanced versions of the SHOP2 HTN planner and the CIRCA Controller Synthesis Module (CSM). Hy-CIRCA’s planning process has 5 steps: (1) Using SHOP2, compute an approximate mission plan. While computing this plan, compute a hybrid automaton model of the plan, featuring more expressive continuous dynamics. (2) Using dReal, solve this hybrid model, establishing the correctness of the plan, and computing values for its continuous parameters. To execute the plan, (3) extract from the plan specifications for closed-loop, hard real-time supervisory controllers for the agents that must execute the plan. (4) Based upon these specifications, use the CIRCA CSM to plan the controllers. To ensure correct execution, (5) verify the CSM-generated controllers with dReal.
A Term Rewriting Approach to Analyze High Level Petri Nets.
Xudong He, Reng Zeng, Su Liu, Zhuo Sun, Kyungmin Bae.
International Symposium on Theoretical Aspects of Software Engineering (TASE 2016).
[abstract] [link]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.
Multirate PALS reduces the design and verification of a virtually synchronous distributed real-time system to the design and verification of the underlying synchronous model. This paper introduces Hybrid Multirate PALS, which extends Multirate PALS to virtually synchronous distributed multirate hybrid systems, such as aircraft and power plant control systems. Such a system may have interrelated local physical environments, each of whose continuous behaviors may periodically change due to actuator commands. We define continuous interrelated local physical environments, and the synchronous and asynchronous Hybrid Multirate PALS models, and give a trace equivalence result relating a synchronous and an asynchronous model. Finally, we illustrate by an example how invariants can be verified using SMT solving.
SMT Encoding of Hybrid Systems in dReal.
Kyungmin Bae, Soonho Kong, and Sicun Gao.
International Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH@CPSWeek 2015).
[abstract] [link]Analysis problems of hybrid systems, involving nonlinear real functions and ordinary differential equations, can be reduced to SMT (satisfiability modulo theories) problems over the real numbers. The dReal solver can automatically check the satisfiability of such SMT formulas up to a given precision δ > 0. This paper explains how bounded model checking problems of hybrid systems are encoded in dReal. In particular, a novel SMT syntax of dReal enables to effectively represent networks of hybrid systems in a modular way. We illustrate SMT encoding in dReal with simple nonlinear hybrid systems.
For an infinite-state concurrent system S with a set AP of state predicates, its predicate abstraction defines a finite-state system whose states are subsets of AP, and its transitions s' -> s' are witnessed by concrete transitions between states in S satisfying the respective sets of predicates s and s'. Since it is not always possible to find such witnesses, an over-approximation adding extra transitions is often used. For systems S described by formal specifications, predicate abstractions are typically built using various automated deduction techniques. This paper presents a new method—based on rewriting, semantic unification, and variant narrowing—to automatically generate a predicate abstraction when the formal specification of S is given by a conditional rewrite theory. The method is illustrated with concrete examples showing that it naturally supports abstraction refinement and is quite accurate, i.e., it can produce abstractions not needing over-approximations.
Many cyber-physical systems are hierarchical distributed control systems whose components operate with different rates, and that should behave in a virtually synchronous way. Designing such systems is hard due to asynchrony, skews of the local clocks, and network delays; furthermore, their model checking is typically unfeasible due to state space explosion. Multirate PALS reduces the problem of designing and verifying virtually synchronous multirate systems to the much simpler tasks of specifying and verifying their underlying synchronous design. To make the Multirate PALS design and verification methodology available within an industrial modeling environment, we define in this paper the modeling language Multirate Synchronous AADL, which can be used to specify multirate synchronous designs using the AADL modeling standard. We then define the formal semantics of Multirate Synchronous AADL in Real-Time Maude, and integrate Real-Time Maude verification into the OSATE tool environment for AADL. Finally, we show how an algorithm for smoothly turning an airplane can be modeled and analyzed using Multirate Synchronous AADL.
The linear temporal logic of rewriting (LTLR) is a simple extension of LTL that adds spatial action patterns to the logic, expressing that a specific instance of an action described by a rewrite rule has been performed. Although the theory and algorithms of LTLR for finite-state model checking are well-developed , no theoretical foundations have yet been developed for infinite-state LTLR model checking. The main goal of this paper is to develop such foundations for narrowing-based logical model checking of LTLR properties. A key theme in this paper is the systematic relationship, in the form of a simulation with remarkably good properties, between the concrete state space and the symbolic state space. A related theme is the use of additional state space reduction methods, such as folding and equational abstractions, that can in some cases yield a finite symbolic state space.
Abstract Logical Model Checking of Infinite-State Systems Using Narrowing.
Kyungmin Bae, Santiago Escobar and José Meseguer.
International Conference on Rewriting Techniques and Applications (RTA 2013).
[abstract] [link]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.
The SynchAADL2Maude Tool.
Kyungmin Bae, Peter Olveczky, José Meseguer, and Abdullah Al-Nayeem.
International Conference on Fundamental Approaches to Software Engineering (FASE 2012).
[abstract] [link]SynchAADL2Maude is an Eclipse plug-in that uses Real-Time Maude to simulate and model check Synchronous AADL models. Synchronous AADL is a variant of the industrial modeling standard AADL that supports the modeling of synchronous embedded systems. In particular, Synchronous AADL can be used to define in AADL the synchronous models in the PALS methodology, in which the very hard tasks of modeling and verifying an asynchronous distributed real-time system that should be virtually synchronous can be reduced to the much simpler tasks of modeling and verifying the underlying synchronous design.
Formal Patterns for Multi-Rate Distributed Real-Time Systems.
Kyungmin Bae, José Meseguer, and Peter Ölveczky.
International Symposium on Formal Aspects of Component Software (FACS 2012).
[abstract] [link]Distributed real-time systems (DRTSs), such as avionics and automotive systems, are very hard to design and verify. Besides the difficulties of asynchrony, clock skews, and network delays, an additional source of complexity comes from the multirate nature of many such systems, which must implement several levels of hierarchical control at different rates. In this work we present several simple model transformations and a multirate extension of the PALS pattern which can be combined to reduce the design and verification of a virtually synchronous multirate DRTS to the much simpler task of specifying and verifying a single synchronous system. We illustrate the ideas with a multirate hierarchical control system where a central controller orchestrates control systems in the ailerons and tail of an airplane to perform turning maneuvers.
PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude.
Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Ölveczky.
International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2012).
[abstract] [link]Distributed cyber-physical systems (DCPS) are pervasive in areas such as aeronautics and ground transportation systems, including the case of distributed hybrid systems. DCPS design and verification is quite challenging because of asynchronous communication, network delays, and clock skews. Furthermore, their model checking verification typically becomes unfeasible due to the huge state space explosion caused by the system's concurrency. The PALS ("physically asynchronous, logically synchronous") methodology has been proposed to reduce the design and verification of a DCPS to the much simpler task of designing and verifying its underlying synchronous version. The original PALS methodology assumes a single logical period, but Multirate PALS extends it to deal with multirate DCPS in which components may operate with different logical periods. This paper shows how Multirate PALS can be applied to formally verify a nontrivial multirate DCPS. We use Real-Time Maude to formally specify a multirate distributed hybrid system consisting of an airplane maneuvered by a pilot who turns the airplane according to a specified angle through a distributed control system. Our formal analysis revealed that the original design was ineffective in achieving a smooth turning maneuver, and led to a redesign of the system that satisfies the desired correctness properties. This shows that the Multirate PALS methodology is not only effective for formal DCPS verification, but can also be used effectively in the DCPS design process, even before properties are verified.
Many temporal logic properties of interest involve both state and action predicates and only hold under suitable fairness assumptions. Temporal logics supporting both state and action predicates such as the Temporal Logic of Rewriting (TLR) can be used to express both the desired properties and the fairness assumptions. However, model checking such properties directly can easily become impossible for two reasons: (i) the exponential blowup in generating the Büchi automaton for the implication formula including the fairness assumptions in its condition easily makes such generation unfeasible; and (ii) often the needed fairness assumptions cannot even be expressed as propositional temporal logic formulas because they are parametric, that is, they correspond to universally quantified temporal logic formulas. Such universal quantification is succinctly captured by the notion of localized fairness; for example, fairness localized to the parameter o in object fairness conditions. We summarize the foundations and present the language design and implementation of the new Maude LTLR Model Checker under localized fairness. This is the first tool we are aware of which can model check temporal logic properties under parametric fairness assumptions.
In modeling a concurrent system, fairness constraints are usually considered at a specific granularity level of the system, leading to many different variants of fairness: transition fairness, object/process fairness, actor fairness, etc. These different notions of fairness can be unified by making explicit their parametrization over the relevant entities in the system as universal quantification. We propose a state/event-based framework as well as an on-the-fly model checking algorithm to verify LTL properties under universally quantified parametric fairness assumptions, specified by generalized strong/weak fairness formulas. It enables verification of temporal properties under fairness conditions associated to dynamic entities such as new process creations. We have implemented our algorithm within the Maude system.
Synchronous AADL and its Formal Analysis in Real-Time Maude.
Kyungmin Bae, Peter Olveczky, Abdullah Al-Nayeem and José Meseguer.
International Conference on Formal Engineering Methods (ICFEM 2011).
[abstract] [link]Distributed Real-Time Systems (DRTS), such as avionics systems and distributed control systems in motor vehicles, are very hard to design because of asynchronous communication, network delays, and clock skews. Furthermore, their model checking problem typically becomes unfeasible due to the large state spaces caused by the interleavings. For many DRTSs, we can use the PALS methodology to reduce the problem of designing and verifying asynchronous DRTSs to the much simpler task of designing and verifying their synchronous versions. AADL is an industrial modeling standard for avionics and automotive systems. We define in this paper the Synchronous AADL language for modeling synchronous real-time systems in AADL, and provide a formal semantics for Synchronous AADL in Real-Time Maude. We have integrated into the OSATE modeling environment for AADL a plug-in which allows us to model check Synchronous AADL models in Real-Time Maude within OSATE. We exemplify such verification on an avionics system, whose Synchronous AADL design can be model checked in less than 10 seconds, but whose asynchronous design cannot be feasibly model checked.
Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models.
Kyungmin Bae and Peter C. Ölveczky.
International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010).
[abstract] [link]This paper extends our Real-Time Maude formalization of the semantics of flat Ptolemy II discrete-event (DE) models to hierarchical models, including modal models. This is a challenging task that requires combining synchronous fixed-point computations with hierarchical structure. The synthesis of a Real-Time Maude verification model from a Ptolemy II DE model, and the formal verification of the synthesized model in Real-Time Maude, have been integrated into Ptolemy II, enabling a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude.
This paper presents the foundation, design, and implementation of the Linear Temporal Logic of Rewriting model checker as an extension of the Maude system. The Linear Temporal Logic of Rewriting (LTLR) extends linear temporal logic with spatial action patterns which represent rewriting events. LTLR generalizes and extends various state-based and event-based logics and aims to avoid certain types of mismatches between a system and its temporal logic properties. We have implemented the LTLR model checker at the C++ level within the Maude system by extending the existing Maude LTL model checker. Our LTLR model checker provides very expressive methods to define event-related properties as well as state-related properties, or, more generally, properties involving both events and state predicates. This greater expressiveness is gained without compromising performance, because the LTLR implementation minimizes the extra costs involved in handling the events of systems.
Verifying Ptolemy II Discrete-Event Models using Real-Time Maude.
Kyungmin Bae, Peter C. Ölveczky, Thomas H. Feng and Stavros Tripakis
International Conference on Formal Engineering Methods (ICFEM 2009).
[abstract] [link]This paper shows how Ptolemy II discrete-event (DE) models can be formally analyzed using Real-Time Maude. We formalize in Real-Time Maude the semantics of a subset of hierarchical Ptolemy II DE models, and explain how the code generation infrastructure of Ptolemy II has been used to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude.
A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting.
Kyungmin Bae and José Meseguer.
International Workshop on Rule-Based Programming (RULE 2008).
Electronic Notes in Theoretical Computer Science 290: 19-36, 2012.
[abstract] [link]This paper presents a model checker for LTLR, a subset of the temporal logic of rewriting TLR\* extending linear temporal logic with spatial action patterns. Both LTLR and TLR\* are very expressive logics generalizing well-known state-based and action-based logics. Furthermore, the semantics of TLR\* is given in terms of rewrite theories, so that the concurrent systems on which the LTLR properties are model checked can be specified at a very high level with rewrite rules. This paper answers a nontrivial challenge, namely, to be able to build a model checker to model check LTLR formulas on rewrite theories with relatively little effort by reusing Maude's LTL model checker for rewrite theories. For this, the reflective features of both rewriting logic and its Maude implementation have proved extremely useful.
Designing and Verifying Distributed Cyber-Physical Systems using Multirate PALS: An Airplane Turning Control System Case Study.
Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Ölveczky.
Science of Computer Programming 103:13-50, 2015.
[abstract] [link]Distributed cyber-physical systems (DCPS), such as aeronautics and ground transportation systems, are very hard to design and verify, because of asynchronous communication, network delays, and clock skews. Their model checking verification typically becomes unfeasible due to the huge state space explosion caused by the system's concurrency. The Multirate PALS ("physically asynchronous, logically synchronous") methodology has been proposed to reduce the design and verification of a DCPS to the much simpler task of designing and verifying its underlying synchronous version, where components may operate with different periods. This paper presents a methodology for formally modeling and verifying multirate DCPSs using Multirate PALS. In particular, this methodology explains how to deal with the system's physical environment in Multirate PALS. We illustrate our methodology with a multirate DCPS consisting of an airplane maneuvered by a pilot, who turns the airplane to a specified angle through a distributed control system. Our formal analysis using Real-Time Maude revealed that the original design did not achieve a smooth turning maneuver, and led to a redesign of the system. We then use model checking and Multirate PALS to prove that the redesigned system satisfies the desired correctness properties, whereas model checking the corresponding asynchronous model is unfeasible. This shows that Multirate PALS is not only effective for formal DCPS verification, but can also be used effectively in the DCPS design process.
This paper presents the linear temporal logic of rewriting (LTLR) model checker under localized fairness assumptions for the Maude system. The linear temporal logic of rewriting extends linear temporal logic (LTL) with spatial action patterns that describe patterns of rewriting events. Since LTLR generalizes and extends various state-based and event-based logics, mixed properties involving both state propositions and actions, such as fairness properties, can be naturally expressed in LTLR. However, often the needed fairness assumptions cannot even be expressed as propositional temporal logic formulas because they are parametric, that is, they correspond to universally quantified temporal logic formulas. Such universal quantification is succinctly captured by the notion of localized fairness; for example, fairness is localized to the object name parameter in object fairness conditions. We summarize the foundations, and present the language design and implementation of the Maude Fair LTLR model checker, developed at the C++ level within the Maude system by extending the existing Maude LTL model checker. Our tool provides not only an efficient LTLR model checking algorithm under parameterized fairness assumptions but also suitable specification languages as part of its user interface. The expressiveness and effectiveness of the Maude Fair LTLR model checker are illustrated by five case studies. This is the first tool we are aware of that can model check temporal logic properties under parameterized fairness assumptions.
Distributed real-time systems (DRTSs), such as avionics and automotive systems, are very hard to design and verify. Besides the difficulties of asynchrony, clock skews, and network delays, an additional source of complexity comes from the multirate nature of many such systems, which must implement several levels of hierarchical control at different rates. In previous work we showed how the design and implementation of a single-rate DRTS which should behave in a virtually synchronous way can be drastically simplified by the PALS model transformation that generates the DRTS from a much simpler synchronous model. In this work we present several simple model transformations and a multirate extension of the PALS pattern which can be combined to reduce the design and verification of a virtually synchronous multirate DRTS to the much simpler task of specifying and verifying a single synchronous system. We illustrate the ideas with a multirate hierarchical control system where a central controller orchestrates control systems in the ailerons and tail of an airplane to perform turning maneuvers.
Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude.
Kyungmin Bae, Peter C. Olveczky, Thomas H. Feng, Edward A. Lee and Stavros Tripakis.
Science of Computer Programming 77(12):1235-1271, 2012.
[abstract] [link]This paper defines a real-time rewriting logic semantics for a significant subset of Ptolemy II discrete-event models. This is a challenging task, since such models combine a synchronous fixed-point semantics with hierarchical structure, explicit time, and a rich expression language. The code generation features of Ptolemy II have been leveraged to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model, and to integrate Real-Time Maude verification of the synthesized model into Ptolemy II. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude. We illustrate such formal verification of Ptolemy II models with three case studies.
Model checking is an automatic technique for verifying concurrent systems. The properties of the system to be verified are typically expressed as temporal logic formulas, while the system itself is formally specified as a certain system specification language, such as computational logics and conventional programming languages. Rewriting logic is a highly expressive computational logic for effectively defining a formal executable semantics of a wide range of system specification languages. This dissertation presents new rewriting-based model checking methods and tools to effectively verify concurrent systems by means of their rewriting-based formal semantics. Specifically, this work develops: (i) efficient model checking algorithms and a tool for a suitable property specification language, namely, linear temporal logic of rewriting (LTLR) formulas under parameterized fairness; (ii) various infinite-state model checking techniques for LTLR properties, such as equational abstraction, folding abstraction, predicate abstraction, and narrowing-based symbolic model checking; and (iii) the Multirate PALS methodology for making it possible to model check virtually synchronous cyber-physical systems by reducing their system complexity. To demonstrate rewriting-based model checking, we have developed fully integrated modeling and model checking tools for two widely-used embedded system modeling languages, AADL and Ptolemy II. This approach provides a model-engineering process that combines the advantages of an existing modeling language with automatic rewriting-based model checking.