2016
 SMTBased 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).
[abstract] [link]
This paper presents general techniques for verifying virtually synchronous distributed control systems with interconnected physical environments. Such cyberphysical 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 realtime 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 CorrectbyConstruction 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 HyCIRCA, an architecture for verified, correctbyconstruction planning and execution for hybrid systems, including nonlinear continuous dynamics. HyCIRCA addresses the high computational complexity of such systems by first planning at an abstract level, and then progressively refining the original plan. HyCIRCA 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, HyCIRCA 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.
AAAI16 Workshop on Planning for Hybrid Systems (PlanHS 2016).
[abstract] [link]This paper describes HyCIRCA, an architecture for verified, correctbyconstruction planning and execution for hybrid systems, including nonlinear continuous dynamics. HyCIRCA addresses the high computational complexity of such systems by first planning at an abstract level, and then progressively refining the original plan. HyCIRCA 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 humanmachine 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. HyCIRCA integrates the dReal nonlinear SMT solver, with enhanced versions of the SHOP2 HTN planner and the CIRCA Controller Synthesis Module (CSM). HyCIRCA’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 closedloop, hard realtime 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 CSMgenerated 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 wellknown 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 wellknown 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.
2015

Hybrid Multirate PALS.
Kyungmin Bae and Peter C. Ölveczky.
Logic, Rewriting, and Concurrency, 2015.
[abstract] [link]Multirate PALS reduces the design and verification of a virtually synchronous distributed realtime 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.
2014

Predicate Abstraction of Rewrite Theories.
Kyungmin Bae and José Meseguer.
Joint International Conference on Rewriting and Typed Lambda Calculi (RTATLCA 2014).
[abstract] [link]For an infinitestate concurrent system S with a set AP of state predicates, its predicate abstraction defines a finitestate 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 overapproximation 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 overapproximations. 
Definition, Semantics, and Analysis of Multirate Synchronous AADL.
Kyungmin Bae, Peter Olveczky, and José Meseguer.
International Symposium on Formal Methods (FM 2014).
[abstract] [link]Many cyberphysical 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 RealTime Maude, and integrate RealTime 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. 
InfiniteState Model Checking of LTLR Formulas Unsing Narrowing.
Kyungmin Bae and José Meseguer.
International Workshop on Rewriting Logic and its Applications (WRLA 2014).
[abstract] [link]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 finitestate model checking are welldeveloped [2], no theoretical foundations have yet been developed for infinitestate LTLR model checking. The main goal of this paper is to develop such foundations for narrowingbased 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.
2013

Abstract Logical Model Checking of InfiniteState 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 overapproximation or an underapproximation of the logical state space: (i) a folding abstraction that collapses patterns into more general ones, (ii) an easytocheck 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 narrowingbased LTL model checker we are aware of.
2012

The SynchAADL2Maude Tool.
Kyungmin Bae, Peter Olveczky, José Meseguer, and Abdullah AlNayeem.
International Conference on Fundamental Approaches to Software Engineering (FASE 2012).
[abstract] [link]SynchAADL2Maude is an Eclipse plugin that uses RealTime 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 realtime 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 MultiRate Distributed RealTime Systems.
Kyungmin Bae, José Meseguer, and Peter Ölveczky.
International Symposium on Formal Aspects of Component Software (FACS 2012).
[abstract] [link]Distributed realtime 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. 
PALSBased Analysis of an Airplane Multirate Control System in RealTime Maude.
Kyungmin Bae, Josh Krisiloff, José Meseguer, and Peter Ölveczky.
International Workshop on Formal Techniques for SafetyCritical Systems (FTSCS 2012).
[abstract] [link]Distributed cyberphysical 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 RealTime 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. 
Model Checking LTLR Formulas under Localized Fairness.
Kyungmin Bae and José Meseguer.
International Workshop on Rewriting Logic and its Applications (WRLA 2012).
[abstract] [link]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.
2011

State/Eventbased LTL Model Checking under Parametric Generalized Fairness.
Kyungmin Bae and José Meseguer.
International Conference on Computer Aided Verification (CAV 2011).
[abstract] [link]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/eventbased framework as well as an onthefly 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 RealTime Maude.
Kyungmin Bae, Peter Olveczky, Abdullah AlNayeem and José Meseguer.
International Conference on Formal Engineering Methods (ICFEM 2011).
[abstract] [link]Distributed RealTime 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 realtime systems in AADL, and provide a formal semantics for Synchronous AADL in RealTime Maude. We have integrated into the OSATE modeling environment for AADL a plugin which allows us to model check Synchronous AADL models in RealTime 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.
2010

Extending the RealTime Maude Semantics of Ptolemy to Hierarchical DE Models.
Kyungmin Bae and Peter C. Ölveczky.
International Workshop on Rewriting Techniques for RealTime Systems (RTRTS 2010).
[abstract] [link]This paper extends our RealTime Maude formalization of the semantics of flat Ptolemy II discreteevent (DE) models to hierarchical models, including modal models. This is a challenging task that requires combining synchronous fixedpoint computations with hierarchical structure. The synthesis of a RealTime Maude verification model from a Ptolemy II DE model, and the formal verification of the synthesized model in RealTime Maude, have been integrated into Ptolemy II, enabling a modelengineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in RealTime Maude. 
The Linear Temporal Logic of Rewriting Maude Model Checker.
Kyungmin Bae and José Meseguer.
International Workshop on Rewriting Logic and its Applications (WRLA 2010).
[abstract] [link]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 statebased and eventbased 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 eventrelated properties as well as staterelated 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.
2009

Verifying Ptolemy II DiscreteEvent Models using RealTime 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 discreteevent (DE) models can be formally analyzed using RealTime Maude. We formalize in RealTime 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 RealTime Maude verification model from a Ptolemy II design model. This enables a modelengineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in RealTime Maude.
2008

A RewritingBased Model Checker for the Linear Temporal Logic of Rewriting.
Kyungmin Bae and José Meseguer.
International Workshop on RuleBased Programming (RULE 2008).
Electronic Notes in Theoretical Computer Science 290: 1936, 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 wellknown statebased and actionbased 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.
2015

Designing and Verifying Distributed CyberPhysical 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:1350, 2015.
[abstract] [link]Distributed cyberphysical 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 RealTime 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. 
Model Checking Linear Temporal Logic of Rewriting Formulas under Localized Fairness.
Kyungmin Bae, and José Meseguer.
Science of Computer Programming 99:193234, 2015.
[abstract] [link]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 statebased and eventbased 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.
2014

Formal Patterns for Multirate Distributed RealTime Systems (extended version).
Kyungmin Ba, José Meseguer, and Peter Ölveczky.
Science of Computer Programming 91:344, 2014.
[abstract] [link]Distributed realtime 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 singlerate 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.
2012

Verifying Hierarchical Ptolemy II DiscreteEvent Models using RealTime Maude.
Kyungmin Bae, Peter C. Olveczky, Thomas H. Feng, Edward A. Lee and Stavros Tripakis.
Science of Computer Programming 77(12):12351271, 2012.
[abstract] [link]This paper defines a realtime rewriting logic semantics for a significant subset of Ptolemy II discreteevent models. This is a challenging task, since such models combine a synchronous fixedpoint 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 RealTime Maude verification model from a Ptolemy II design model, and to integrate RealTime Maude verification of the synthesized model into Ptolemy II. This enables a modelengineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in RealTime Maude. We illustrate such formal verification of Ptolemy II models with three case studies.
2014

Rewritingbased model checking methods.
Kyungmin Bae.
Ph.D. Thesis, Department of Computer Science, University of Illinois at UrbanaChampaign, 2014.
[abstract] [link]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 rewritingbased model checking methods and tools to effectively verify concurrent systems by means of their rewritingbased 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 infinitestate model checking techniques for LTLR properties, such as equational abstraction, folding abstraction, predicate abstraction, and narrowingbased symbolic model checking; and (iii) the Multirate PALS methodology for making it possible to model check virtually synchronous cyberphysical systems by reducing their system complexity. To demonstrate rewritingbased model checking, we have developed fully integrated modeling and model checking tools for two widelyused embedded system modeling languages, AADL and Ptolemy II. This approach provides a modelengineering process that combines the advantages of an existing modeling language with automatic rewritingbased model checking.