-
Timed Strategies for Real-Time Rewrite Theories
Authors:
Carlos Olarte,
Peter Csaba Ölveczky
Abstract:
In this paper we propose a language for conveniently defining a wide range of execution strategies for real-time rewrite theories, and provide Maude-strategy-implemented versions of most Real-Time Maude analysis methods, albeit with user-defined discrete and timed strategies. We also identify a new time sampling strategy that should provide both efficient and exhaustive analysis for many distribut…
▽ More
In this paper we propose a language for conveniently defining a wide range of execution strategies for real-time rewrite theories, and provide Maude-strategy-implemented versions of most Real-Time Maude analysis methods, albeit with user-defined discrete and timed strategies. We also identify a new time sampling strategy that should provide both efficient and exhaustive analysis for many distributed real-time systems. We exemplify the use of our language and its analyses on a simple round trip time protocol, and compare the performance of standard Maude search with our strategy-implemented reachability analyses on the CASH scheduling algorithm benchmark.
△ Less
Submitted 13 March, 2024;
originally announced March 2024.
-
A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
Authors:
Jaime Arias,
Kyungmin Bae,
Carlos Olarte,
Peter Csaba Ölveczky,
Laure Petrucci
Abstract:
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 comp…
▽ More
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 analysis 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 Romeo 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 Romeo in many cases.
△ Less
Submitted 12 September, 2024; v1 submitted 3 January, 2024;
originally announced January 2024.
-
Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving
Authors:
Jaime Arias,
Kyungmin Bae,
Carlos Olarte,
Peter Csaba Ölveczky,
Laure Petrucci,
Fredrik Rømming
Abstract:
Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding a…
▽ More
Parametric time Petri nets with inhibitor arcs (PITPNs) support flexibility for timed systems by allowing parameters in firing bounds. In this paper we present and prove correct a concrete and a symbolic rewriting logic semantics for PITPNs. We show how this allows us to use Maude combined with SMT solving to provide sound and complete formal analyses for PITPNs. We develop a new general folding approach for symbolic reachability that terminates whenever the parametric state-class graph of the PITPN is finite. We explain how almost all formal analysis and parameter synthesis supported by the state-of-the-art PITPN tool Roméo can be done in 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 on three benchmarks show that our methods outperform Roméo in many cases.
△ Less
Submitted 15 March, 2023;
originally announced March 2023.
-
PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude
Authors:
Kyungmin Bae,
Joshua Krisiloff,
José Meseguer,
Peter Csaba Ölveczky
Abstract:
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 expl…
▽ More
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.
△ Less
Submitted 31 December, 2012;
originally announced January 2013.
-
Proceedings First International Workshop on Formal Techniques for Safety-Critical Systems
Authors:
Peter Csaba Ölveczky,
Cyrille Artho
Abstract:
This volume contains the proceedings of the First International Workshop of Formal Techniques for Safety-Critical Systems (FTSCS 2012), held in Kyoto on November 12, 2012, as a satellite event of the ICFEM conference.
The aim of this workshop is to bring together researchers and engineers interested in the application of (semi-)formal methods to improve the quality of safety-critical computer sy…
▽ More
This volume contains the proceedings of the First International Workshop of Formal Techniques for Safety-Critical Systems (FTSCS 2012), held in Kyoto on November 12, 2012, as a satellite event of the ICFEM conference.
The aim of this workshop is to bring together researchers and engineers interested in the application of (semi-)formal methods to improve the quality of safety-critical computer systems. FTSCS is particularly interested in industrial applications of formal methods. Topics include:
- the use of formal methods for safety-critical and QoS-critical systems, including avionics, automotive, and medical systems; - methods, techniques and tools to support automated analysis, certification, debugging, etc.; - analysis methods that address the limitations of formal methods in industry; - formal analysis support for modeling languages used in industry, such as AADL, Ptolemy, SysML, SCADE, Modelica, etc.; and - code generation from validated models.
The workshop received 25 submissions; 21 of these were regular papers and 4 were tool/work-in-progress/position papers. Each submission was reviewed by three referees; based on the reviews and extensive discussions, the program committee selected nine regular papers, which are included in this volume. Our program also included an invited talk by Ralf Huuck.
△ Less
Submitted 28 December, 2012;
originally announced December 2012.
-
Formal Visual Modeling of Real-Time Systems in e-Motions: Two Case Studies
Authors:
Francisco Durán,
Peter Csaba Ölveczky,
José E. Rivera
Abstract:
e-Motions is an Eclipse-based visual timed model transformation framework with a Real-Time Maude semantics that supports the usual Maude formal analysis methods, including simulation, reachability analysis, and LTL model checking. e-Motions is characterized by a novel and powerful set of constructs for expressing timed behaviors. In this paper we illustrate the use of these constructs --- and t…
▽ More
e-Motions is an Eclipse-based visual timed model transformation framework with a Real-Time Maude semantics that supports the usual Maude formal analysis methods, including simulation, reachability analysis, and LTL model checking. e-Motions is characterized by a novel and powerful set of constructs for expressing timed behaviors. In this paper we illustrate the use of these constructs --- and thereby implicitly investigate their suitability to define real-time systems in an intuitive way --- to define and formally analyze two prototypical and very different real-time systems: (i) a simple round trip time protocol for computing the time it takes a message to travel from one node to another, and back; and (ii) the EDF scheduling algorithm.
△ Less
Submitted 30 June, 2011;
originally announced July 2011.
-
Formal Model Engineering for Embedded Systems Using Real-Time Maude
Authors:
Peter Csaba Ölveczky
Abstract:
This paper motivates why Real-Time Maude should be well suited to provide a formal semantics and formal analysis capabilities to modeling languages for embedded systems. One can then use the code generation facilities of the tools for the modeling languages to automatically synthesize Real-Time Maude verification models from design models, enabling a formal model engineering process that comb…
▽ More
This paper motivates why Real-Time Maude should be well suited to provide a formal semantics and formal analysis capabilities to modeling languages for embedded systems. One can then use the code generation facilities of the tools for the modeling languages to automatically synthesize Real-Time Maude verification models from design models, enabling a formal model engineering process that combines the convenience of modeling using an informal but intuitive modeling language with formal verification. We give a brief overview six fairly different modeling formalisms for which Real-Time Maude has provided the formal semantics and (possibly) formal analysis. These models include behavioral subsets of the avionics modeling standard AADL, Ptolemy II discrete-event models, two EMF-based timed model transformation systems, and a modeling language for handset software.
△ Less
Submitted 30 June, 2011;
originally announced July 2011.
-
Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family
Authors:
Peter Csaba Ölveczky,
José Meseguer
Abstract:
Distributed embedded systems (DESs) are no longer the exception; they are the rule in many application areas such as avionics, the automotive industry, traffic systems, sensor networks, and medical devices. Formal DES specification and verification is challenging due to state space explosion and the need to support real-time features. This paper reports on an extensive industry-based case study…
▽ More
Distributed embedded systems (DESs) are no longer the exception; they are the rule in many application areas such as avionics, the automotive industry, traffic systems, sensor networks, and medical devices. Formal DES specification and verification is challenging due to state space explosion and the need to support real-time features. This paper reports on an extensive industry-based case study involving a DES product family for a pedestrian and car 4-way traffic intersection in which autonomous devices communicate by asynchronous message passing without a centralized controller. All the safety requirements and a liveness requirement informally specified in the requirements document have been formally verified using Real-Time Maude and its model checking features.
△ Less
Submitted 22 September, 2010;
originally announced September 2010.
-
Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications
Authors:
Daniela Lepri,
Peter Csaba Ölveczky,
Erika Ábrahám
Abstract:
This paper presents a transformational approach for model checking two important classes of metric temporal logic (MTL) properties, namely, bounded response and minimum separation, for nonhierarchical object-oriented Real-Time Maude specifications. We prove the correctness of our model checking algorithms, which terminate under reasonable non-Zeno-ness assumptions when the reachable state space is…
▽ More
This paper presents a transformational approach for model checking two important classes of metric temporal logic (MTL) properties, namely, bounded response and minimum separation, for nonhierarchical object-oriented Real-Time Maude specifications. We prove the correctness of our model checking algorithms, which terminate under reasonable non-Zeno-ness assumptions when the reachable state space is finite. These new model checking features have been integrated into Real-Time Maude, and are used to analyze a network of medical devices and a 4-way traffic intersection system.
△ Less
Submitted 22 September, 2010;
originally announced September 2010.
-
A Rewriting-Logic-Based Technique for Modeling Thermal Systems
Authors:
Muhammad Fadlisyah,
Erika Ábrahám,
Daniela Lepri,
Peter Csaba Ölveczky
Abstract:
This paper presents a rewriting-logic-based modeling and analysis technique for physical systems, with focus on thermal systems. The contributions of this paper can be summarized as follows: (i) providing a framework for modeling and executing physical systems, where both the physical components and their physical interactions are treated as first-class citizens; (ii) showing how hea…
▽ More
This paper presents a rewriting-logic-based modeling and analysis technique for physical systems, with focus on thermal systems. The contributions of this paper can be summarized as follows: (i) providing a framework for modeling and executing physical systems, where both the physical components and their physical interactions are treated as first-class citizens; (ii) showing how heat transfer problems in thermal systems can be modeled in Real-Time Maude; (iii) giving the implementation in Real-Time Maude of a basic numerical technique for executing continuous behaviors in object-oriented hybrid systems; and (iv) illustrating these techniques with a set of incremental case studies using realistic physical parameters, with examples of simulation and model checking analyses.
△ Less
Submitted 22 September, 2010;
originally announced September 2010.
-
Extending the Real-Time Maude Semantics of Ptolemy to Hierarchical DE Models
Authors:
Kyungmin Bae,
Peter Csaba Ölveczky
Abstract:
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…
▽ More
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.
△ Less
Submitted 22 September, 2010;
originally announced September 2010.
-
Proceedings First International Workshop on Rewriting Techniques for Real-Time Systems
Authors:
Peter Csaba Ölveczky
Abstract:
This volume contains the proceedings of the First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010), held in Longyearbyen, Spitsbergen, on April 6-9, 2010.
The aim of the workshop is to bring together researchers with an interest in the use of rewriting-based techniques (including rewriting logic) and tools for the modeling, analysis, and/or implementation of…
▽ More
This volume contains the proceedings of the First International Workshop on Rewriting Techniques for Real-Time Systems (RTRTS 2010), held in Longyearbyen, Spitsbergen, on April 6-9, 2010.
The aim of the workshop is to bring together researchers with an interest in the use of rewriting-based techniques (including rewriting logic) and tools for the modeling, analysis, and/or implementation of real-time and hybrid systems, and to give them the opportunity to present their recent works, discuss future research directions, and exchange ideas. The topics of the workshop comprise, but are not limited to: methods and tools supporting rewriting-based modeling and analysis of real-time and hybrid systems, and extensions of such systems; use of rewriting techniques to provide rigorous support for model-based software engineering of timed systems; applications and case studies; and comparison with other formalisms and tools.
△ Less
Submitted 20 September, 2010;
originally announced September 2010.
