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

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

Today’s distributed systems must satisfy bothqualitativeandquantitativeproperties. These properties are analyzed using very different formal frameworks: expressive untimed and non-probabilistic frameworks, such as TLA+ and Hoare/separation logics, for qualitative properties; and timed/probabilistic-automaton-based ones, such as Uppaal and Prism, for quantitative ones. This requires developing two quite different models of the same system, without guarantees of semantic consistency between them. Furthermore, it is very hard or impossible torepresentintrinsic features of distributed object systems—such as unbounded data structures, dynamic object creation, and an unbounded number of messages—using finite automata. In this paper we bridge this semantic gap, overcome the problem of manually having to develop two different models of a system, and solve the representation problem by: (i) defining a transformation from a very general class of distributed systems (a generalization of Agha’s actor model) that maps an untimed non-probabilistic distributed system model suitable for qualitative analysis to a probabilistic timed model suitable for quantitative analysis; and (ii) proving the two models semantically consistent. We formalize our models in rewriting logic, and can therefore use the Maude tool to analyze qualitative properties, and statistical model checking with PVeStA to analyze quantitative properties. We have automated this transformation and integrated it, together with the PVeStA statistical model checker, into theActors2PMaudetool. We illustrate the expressiveness of our framework and our tool’s ease of use by automatically transforming untimed, qualitative models of numerous distributed system designs—including an industrial data store and a state-of-the-art transaction system—into quantitative models to analyze and compare the performance of different designs.

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

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

Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.

Abstract Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) (either all or none of a transaction’s updates are visible to other transactions) and prevention of lost updates (PLU). Existing distributed transaction systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency ), but this comes at the price of lower performance. In this paper we propose a new distributed transaction protocol, ROLA, that targets application scenarios where only RA and PLU are needed. We formally specify ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness, we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) perform statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by also modeling and analyzing in Maude the well-known protocols Walter and Jessy that also guarantee RA and PLU. Our statistical model checking results show that ROLA outperforms both Walter and Jessy.

Designers of distributed database systems face the choice between stronger consistency guarantees and better performance. A number of applications only require read atomicity (RA) and prevention of lost updates (PLU). Existing distributed database systems that meet these requirements also provide additional stronger consistency guarantees (such as causal consistency ), and therefore incur lower performance. In this paper we define a new distributed transaction protocol, ROLA, that targets applications where only RA and PLU are needed. We formally model ROLA in Maude. We then perform model checking to analyze both the correctness and the performance of ROLA. For correctness , we use standard model checking to analyze ROLA’s satisfaction of RA and PLU. To analyze performance we: (a) use statistical model checking to analyze key performance properties; and (b) compare these performance results with those obtained by analyzing in Maude the well-known protocol Walter. Our results show that ROLA outperforms Walter.

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.

This paper describes the application of Real-Time Maude to the formal modeling, simulation, and model checking analysis of the NORM multicast protocol standard being developed by the Internet Engineering Task Force. Because of its size and sophistication, real-time features, and the need to model and analyze subcomponents of NORM both in isolation and in combination, NORM poses a set of challenging problems for its formal specification and analysis. Our formal modeling and analysis efforts made us aware of ambiguities, inconsistencies, and cases of under-specification in the informal specification of NORM. Our work indicates that formal methods can successfully be applied by non-experts during the development of advanced Internet protocol standards.

This paper presents general techniques for formally modeling, simulating, and model checking real-time resource-sharing protocols in Real-Time Maude. The "scheduling subset" of our techniques has been used to find a previously unknown subtle bug in a state-of-the-art scheduling algorithm. This paper also shows how our general techniques can be instantiated to model and analyze the well known priority inheritance protocol.

This paper investigates the suitability of applying the general-purpose real-time Maude tool to the formal specification and model checking analysis of time-dependent cryptographic protocols. We restrict the intruders so that they become non-Zeno, and propose a complete analysis method for finding attacks that are reachable from the initial state. Our method has been used on the benchmark wide-mouthed frog (WMF) and Kerberos protocols, on which we can find all the well known flaws in short time. We use the WMF protocol to illustrate formal specification and the use of our method to analyze timed authentication properties.

Advanced wireless sensor network algorithms pose challenges to their formal modeling and analysis, such as modeling probabilistic and real-time behaviors and novel forms of communication, and analyzing both correctness and performance. In this paper, we propose using Real-Time Maude to formally model, simulate, and further analyze such algorithms. The Real-Time Maude formalism is expressive yet intuitive, and the tool provides a spectrum of analysis methods, including simulation, reachability analysis, and temporal logic model checking. We have used Real-Time Maude to formally model and analyze the sophisticated OGDC algorithm. We could perform all the analyses performed by the OGDC developers using the simulation tool ns-2, as well as further analyses which are beyond the capabilities of simulation tools. To the best of our knowledge, this is the first time a formal tool has been applied to such a complex wireless sensor network algorithm.