Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Ölveczky, Laure Petrucci, Fredrik Rømming.
This paper presents a rewriting logic semantics for parametric timed automata (PTAs) and shows that symbolic reachability analysis using Maude-with-SMT is sound and complete for the PTA reachability problem. We then refine standard Maude-with-SMT reachability analysis so that the analysis terminates when the symbolic state space of the PTA is finite. We show how we can synthesize parameters with our methods, and compare their performance with Imitator, a state-of-the-art tool for PTAs. The practical contributions are two-fold: providing new analysis methods for PTAs---e.g. allowing more general state properties in queries and supporting reachability analysis combined with user-defined execution strategies---not supported by Imitator, and developing symbolic analysis methods for real-time rewrite theories.
Byeongjee Kang and Kyungmin Bae.
A concurrent system specified as a rewrite theory can be symbolically analyzed using narrowing-based reachability analysis. Narrowing-based approaches have been applied to formally analyze cryptographic protocols and parameterized protocols. However, existing narrowing-based techniques, based on a breadth-first-search strategy, cannot deal with generic distributed systems with objects and messages due to the symbolic state-space explosion problem. This paper proposes a heuristic search approach for narrowing-based reachability analysis to guide the search for counterexamples involving a small number of objects. As a result, our method can effectively find a counterexample if an error state is reachable. We demonstrate the effectiveness of our technique using a nontrivial distributed consensus algorithm.
Jaeseo Lee, Sangki Kim, and Kyungmin Bae.
A programmable logic controller (PLC) is widely used in industrial control systems, and Structured text (ST) is an imperative language to develop PLC programs. Because of its safety-critical nature, formally analyzing PLC programs is important, and a rewriting-based formal semantics of ST has been proposed for this purpose. This paper presents a bounded model checking technique for PLC ST programs based on the rewriting-based semantics. We apply rewriting modulo SMT to symbolically analyze LTL properties of ST programs with respect to sequences of (possibly infinite) inputs and outputs. We have demonstrated the effectiveness of our approach using a traffic light case study.
Jueun Yeon, Seunghyun Chae, and Kyungmin Bae.
Deep learning has performed well in many areas. However, deep learning is vulnerable to errors such as adversarial examples. Therefore, much research exists on ensuring the safety and robustness of deep neural networks. Since deep neural networks are large in scale and the activation functions are non-linear, linear approximation methods for such activation functions are proposed and widely used for verification. In this paper, we propose a new technique, called layered abstraction, for non-linear activation functions, such as ReLU and Tanh, and the verification algorithm based on that. We have implemented our method by extending the existing SMT-based methods. The experimental evaluation showed that our tool performs better than an existing tool.
Jaehun Lee, Kyungmin Bae, and Peter Csaba Ölveczky.
Many collective adaptive systems consist of distributed nodes that communicate with each other and with their physical environments, but that logically should operate in a synchronous way. HybridSynchAADL is a recent modeling language and formal analysis tool for such virtually synchronous cyber-physical systems (CPSs). HybridSynchAADL uses the Hybrid PALS equivalence to reduce the hard problem of designing and verifying virtually synchronous CPSs—with network delays, asynchronous communication, imprecise local clocks, continuous dynamics, etc.—to the much easier tasks of designing and verifying their underlying synchronous designs. Up to now HybridSynchAADL has lacked important programming language features, such as compound data types and user-defined functions, which made it difficult to model advanced control logics of collective adaptive systems. In this paper, we extend the HybridSynchAADL language, its formal semantics, and its analysis tool to support these programming language features. We apply our extension of HybridSynchAADL to design and analyze a collection of collaborating autonomous drones that adapt to their environments.
Geunyeol Yu, Jia Lee, Kyungmin Bae.
We present the STLmc model checker for signal temporal logic (STL) properties of hybrid systems. The STLmc tool 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. If STLmc does not find a counterexample, the system is guaranteed to be correct up to the given bounds and robustness threshold. We demonstrate the effectiveness of STLmc on a number of hybrid system benchmarks.
Jaehun Lee, Kyungmin Bae, Peter Csaba Ölveczky, Sharon Kim, and Minseok Kang.
This paper presents the HybridSynchAADL modeling language and formal analysis tool for virtually synchronous cyber-physical systems with complex control programs, continuous behaviors, and bounded clock skews, network delays, and execution times. We leverage the Hybrid PALS methodology, so that it is sufficient to model and verify the much simpler underlying synchronous designs. We define the HybridSynchAADL language as a sublanguage of the avionics modeling standard AADL for modeling such synchronous designs in AADL. We define the formal semantics of HybridSynchAADL using Maude with SMT solving, which allows us to represent advanced control programs and communication features in Maude, while capturing timing uncertainties and continuous behaviors symbolically with SMT solving. We have developed new general methods for optimizing the performance of such symbolic rewriting, which makes the analysis of HybridSynchAADL models feasible. We have integrated the formal modeling and analysis of HybridSynchAADL models into the OSATE tool environment for AADL. Finally, we demonstrate the effectiveness of the Hybrid PALS methodology and HybridSynchAADL on a number of applications, including autonomous drones that collaborate to achieve common goals, and compare the performance of our tool with other state-of-the-art formal tools for hybrid systems.
Jia Lee, Geunyeol Yu, Kyungmin Bae.
Signal temporal logic (STL) is widely used to specify and analyze properties of cyber-physical systems with continuous behaviors. But STL model checking is still quite limited; 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 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 modular 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.
MSYNC: A Generalized Formal Design Pattern for Virtually Synchronous Multirate Cyber-physical Systems
Kyungmin Bae and Peter Csaba Ölveczky.
TA 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.
Jaehun Lee, Sharon Kim, Kyungmin Bae and, Peter Csaba Ölveczky.
We present the HYBRIDSYNCHAADL 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 HYBRIDSYNCHAADL language as a sublanguage of the avionics modeling standard AADL for modeling such designs in AADL, and demonstrate the effectiveness of HYBRIDSYNCHAADL on a number of applications.
Geunyeol Yu and Kyungmin Bae.
This paper presents Maude-SE, an SMT extension of Maude that tightly integrates Maude and SMT solvers with extra functionality. In addition to the existing SMT solving capability of Maude, the tool provides three additional features that are not currently supported by Maude but that are very useful for rewriting modulo SMT: (i) building satisfying assignments by SMT solving, (ii) simplifying formulas using the underlying SMT solver, and (iii) dealing with non-linear arithmetic formulas. Hence, Maude-SE can analyze nontrivial systems that cannot be dealt with by the previous Maude-SMT implementation.
Jueun Yeon, Seunghyun Chae, and Kyungmin Bae.
딥 러닝은 다양한 분야에서 좋은 성과를 내고 있지만 그 결과 값이 어떻게 도출되었는지 알 수 없어서 적대적 예제와 같은 오류에 취약하다. 따라서 심층 신경망(deep neural network)의 안전성과 강건성을 보장하기 위한 많은 연구가 이루어지고 있다. 심층 신경망은 규모가 크고 활성화 함수(activation function)들이 비선형이기 때문에 일반적으로 검증 시 활성화 함수를 선형으로 근사하는 방법이 제안되어 널리 사용되고 있다. 본 논문에서는 ReLU, Tanh 등의 활성화 함수에 대해 새로운 근사 방법인 계층별 요약(layered abstraction) 및 이에 기반한 검증 알고리즘을 제안한다. 알고리즘의 구현을 위해 기존의 SMT 기반 방식을 확장하였으며 심층 신경망이 안전한 경우에 대해 효과적으로 동작함을 보인다.
Moonhyeon Jung and Kyungmin Bae.
심층신경망(Deep neural network, DNN)은 음성 인식, 이미지 분류 등의 다양한 분야에서 소프트웨어를 위하여 널리 활용되고 있다. 하지만 DNN에는 적대적 예제와 같은 예상치 못한 오류가 존재할 수 있으 며, 이를 방지하기 위하여 DNN의 요구사항을 검증하기 위한 DNN 정형검증 기술이 활발하게 연구되고 있다. 본 논문에서는 DNN의 요구사항 검증의 성능을 향상하기 위하여 DNN의 구조적 성질을 활용하는 방법론을 제안한다. 본 논문에서는 ReLU를 활성함수로 가지는 DNN의 구조적 성질을 정의하고, 이를 이 용하여 SMT 기반 DNN 검증의 성능을 향상시킬 수 있음을 보였다.
HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous Cyber-Physical Systems in AADL.
Department of Computer Science and
Engineering, Pohang University of
Science and Technology, 2020.
This thesis presents HybridSynchAADL, techniques for desigining and analyzing virtually synchronous cyber-physical systems. Cyber-physical systems (CPSs) are distributed embedded systems that invlove both discrete and continuous components. Many CPSs are virtually synchronous; i.e., the implementation is physically distributed, but the logical design behaves synchronously. Virtually synchronous CPSs are used in many areas, including avionics, automotive, and robotics. Moreover, these systems are often safety-critical, i.e., malfunctions or errors can lead to enormous damage, even human injuries or deaths. Thus, verification of virtually synchronous CPSs is crucial. Designing and anlyzing such system is difficult due to the combination of distributed characteristics and the continuous dynamics of physical environments. Formal verification can be used to analyze such complex CPSs but there are no sufficient tools and methods to verify virtually synchronous CPSs. We introduce HybridSynchAADL to model and analyze such CPSs. HybridSynchAADL models CPSs using the language that extends AADL. The semantics of HybridSynchAADL is formally specified in rewriting modulo SMT. We have implemented a tool that provides a formal analysis capability based on our semantics. We show the effectiveness of the proposed approach by experimenting the case studies on complex CPSs, such as distributed control of drones.
Sharon Kim and Kyungmin Bae.
Jaeseo Lee, Tae-Hyoung Choi, Gyuho Lee, Jaegwan Yu, and Kyungmin Bae.
Code transformation is widely used to improve the performance and security of programs, but serious software errors can occur in this process if the generated program is not equivalent to the original program. There are a number of approaches for translation validation that can be used to prove the equivalence of programs, but the high cost of proof checking restricts the applicability of these techniques for large programs. In this paper, we propose a practical approach for checking the correctness of LLVM code transformation. We first prove the correctness of the transformation rules using automated theorem proving before compilation. We then perform a simple code analysis method—as opposed to directly proving the program equivalence— to check whether the transformations rules are correctly applied to the generated code. As the complexity of the proposed code analysis is linear, our technique can be effectively applied to large programs, unlike previous techniques. To prove the effectiveness of the proposed approach, we present a case study on LLVM code transformation for a code pointer integrity instrumentation.
Kyungmin Bae and Camilo Rocha.
Rewriting modulo SMT is a novel symbolic technique to model and analyze infinite-state systems that interact with a non-deterministic environment, by seamlessly combining rewriting modulo equational theories, SMT solving, and model checking. This paper presents guarded terms, an approach to deal with the symbolic state-space explosion problem for rewriting modulo SMT, one of the main challenges of this technique. 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.
Kyungmin Bae and Jia Lee.
ACM SIGPLAN Symposium on
Principles of Programming Languages
(POPL 2019), accepted for presentation.
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.
Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, October 10-12, 2018, Proceedings.
Kyungmin Bae and Peter Ölveczky.
Lecture Notes in Computer
Science 11222, Springer, 2018.
Modular SMT-Based Analysis of Nonlinear Hybrid Systems.Bounded Model Checking of Signal Temporal Logic Properties Using Syntactic Separation.
Kyungmin Bae and Sicun Gao.
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.
done2017 Best paper
Kyungmin Bae and Camilo Rocha.
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.
Kyungmin Bae, Peter Ölveczky, Soonho Kong, Sicun Gao, and Edmund M. Clarke.
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.
Robert P. Goldman, Daniel Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae.
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.
Robert P. Goldman, Daniel Bryce, Michael J. S. Pelican, David J. Musliner, Kyungmin Bae.
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.
Xudong He, Reng Zeng, Su Liu, Zhuo Sun, Kyungmin Bae.
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.
Kyungmin Bae and Peter C. Ölveczky.
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.
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.
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.
Kyungmin Bae, Soonho Kong, and Sicun Gao.
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.
Kyungmin Bae, and José Meseguer.
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.
Kyungmin Bae and José Meseguer.
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.
Kyungmin Ba, José Meseguer, and Peter Ölveczky.
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.
Kyungmin Bae, Peter Olveczky, and José Meseguer.
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.
Kyungmin Bae and José Meseguer.
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.
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.
Kyungmin Bae, Santiago Escobar and José Meseguer.
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.
Kyungmin Bae, Peter Olveczky, José Meseguer, and Abdullah Al-Nayeem.
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.
Kyungmin Bae, José Meseguer, and Peter Ölveczky.
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.
Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Ölveczky.
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.
Kyungmin Bae and José Meseguer.
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.
Kyungmin Bae, Peter C. Olveczky, Thomas H. Feng, Edward A. Lee and Stavros Tripakis.
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.
Kyungmin Bae and José Meseguer.
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.
Kyungmin Bae, Peter Olveczky, Abdullah Al-Nayeem and José Meseguer.
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.
Kyungmin Bae and Peter C. Ölveczky.
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.
Kyungmin Bae and José Meseguer.
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.
Kyungmin Bae, Peter C. Ölveczky, Thomas H. Feng and Stavros Tripakis
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.
Kyungmin Bae and José Meseguer.
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.