Abstract Effective water management in underground mining requires maintaining safe reservoir levels while minimizing the high energy costs of continuous pumping. Although flexible electricity pricing enables cost-aware operation, traditional threshold-based controllers cannot exploit this flexibility efficiently. This paper presents an industrial case study on efficient mine dewatering using reinforcement-learning-based control synthesized with the Uppaal Stratego framework. A baseline threshold controller is first implemented, followed by a reinforcement-learning controller trained on forecast inflows and day-ahead electricity prices to minimize pumping costs while limiting pump switching. To ensure safety during learning without distorting the optimization objective, we introduce a pre-shield that blocks unsafe transitions. We formally show that this pre-shield is maximally permissive with respect to a monotonicity safety objective. Simulation results demonstrate that the learning-based strategy reduces total energy consumption by up to 40% compared to threshold-based control, while maintaining safe operation in all scenarios.

To address safety concerns in industrial systems, we propose a framework for forecasting CPU load with respect to a predetermined threshold, allowing customers to add tasks from a predefined library. Existing tools, akin to Windows Task Manager, provide limited insights due to their aggregate nature and high computational overhead. Our approach uses conformal prediction for rapid uncertainty-aware forecasts and Shapley value analysis to quantify individual task contributions to the CPU load. This proof-of-concept framework improves system safety assessment by addressing key research questions in load prediction and validation, paving the way for refined measurement methodologies in industrial applications.

As industrial PLC programs become more complex, automated testing and verification methods are needed to ensure their reliability and correctness. This paper presents PyLC+, a modular framework that translates PLC programs into Python, allowing for automated AI-driven test generation. PyLC+ builds upon our previous work, addressing limitations by adopting a class-based modular architecture that improves the tool’s scalability, maintainability, and extensibility. This structural refinement eliminates reliance on nested functions, facilitating the translation of large-scale, real-world PLC programs while maintaining precise use of cyclic execution. Furthermore, PyLC+ introduces automated handling of stateful FBs, ensuring compliance with IEC 61131-3 execution semantics.Additionally, the tool proposes integrating LLM-driven test generation with search-based test generation to improve the efficiency and effectiveness of testing PLC software. We tested PyLC+ in a large-scale company developing train control systems, demonstrating its efficiency and effectiveness in handling complex industrial PLC programs.

Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

Abstract This paper proposes an approach to pattern-based modeling and Uppaal-based verification for ROS 2 applications. The proposed verification focuses on callback execution latencies and buffer overflow. We propose formal model templates to model the execution of ROS 2 system components, created using a pattern-based approach. The model templates simplify the formal modeling of an ROS 2 application. Using Uppaal, we model in Uppaal timed automata, allowing the description of computation chains of ROS 2-based applications. Our focus is on execution behavior, including two versions of the mainline single-threaded executor of ROS 2. System traces generated using the formal models are validated in multiple experiments. Furthermore, we compare two approaches to modeling the execution of nodes that are typically the core units of computation of ROS 2. The first approach is a holistic approach to model ROS 2 applications, including communication and execution in computation chains. The second is an approach for individual nodes only, at a higher abstraction level. Additionally, we show the application of the verification by model checking in two ROS 2 system scenarios where we compare generated model traces to actual system executions. Overall, through formal modeling and verification, we showcase the potential for uncovering errors in the execution of distributed robotic systems.

Abstract Integrating machine learning into computer architecture simulation offers a new approach to performance analysis, moving away from traditional algorithmic methods. While existing simulators accurately replicate hardware, they often suffer from slow execution, complex documentation, and require deep CPU knowledge, limiting their usability for quick insights. This paper presents a deep learning-based approach for simulating a key CPU component, cache memory. Our model “learns” cache characteristics by observing cache miss distributions, without needing detailed manual modeling. This method accelerates simulations and adapts to different program needs, demonstrating accuracy comparable to traditional simulators. Tested on Sysbench and image processing algorithms, it shows promise for faster, scalable, and hardware-independent simulations.

Mission planning for multi-agent autonomous systems aims to generate feasible and optimal mission plans that satisfy given requirements. In this article, we propose a tool-supported mission-planning methodology that combines (i) a path-planning algorithm for synthesizing path plans that are safe in environments with complex road conditions, and (ii) a task-scheduling method for synthesizing task plans that schedule the tasks in the right and fastest order, taking into account the planned paths. The task-scheduling method is based on model checking, which provides means of automatically generating task execution orders that satisfy the requirements and ensure the correctness and efficiency of the plans by construction. We implement our approach in a tool named MALTA, which offers a user-friendly GUI for configuring mission requirements, a module for path planning, an integration with the model checker UPPAAL, and functions for automatic generation of formal models, and parsing of the execution traces of models. Experiments with the tool demonstrate its applicability and performance in various configurations of an industrial case study of an autonomous quarry. We also show the adaptability of our tool by employing it in a special case of an industrial case study.

Numerous industrial sectors employ Programmable Logic Controllers (PLC) software to control safety-critical systems. These systems necessitate extensive testing and stringent coverage measurements, which can be facilitated by automated test-generation techniques. Existing such techniques have not been applied to PLC programs, and therefore do not directly support the latter regarding automated test-case generation. To address this deficit, in this work, we introduce PyLC, a tool designed to automate the conversion of PLC programs to Python code, assisted by an existing test generator called Pynguin. Our framework is capable of handling PLC programs written in the Function Block Diagram language. To demonstrate its capabilities, we employ PyLC to transform safety-critical programs from industry and illustrate how our approach can facilitate the manual and automatic creation of tests. Our study highlights the efficacy of leveraging Python as an intermediary language to bridge the gap between PLC development tools, Python-based unit testing, and automated test generation.

Robot operating system 2 (ROS 2) is increasingly popular both in research and commercial robotic systems. ROS 2 is designed to allow real-time execution and data communication, enabling rapid prototyping and deployment of robotic systems. In order to predict and calculate execution times in ROS 2, one needs to analyze its internal scheduler, called executor. The executor has been updated in various distributions of ROS 2, which is shown to impact significantly the periodic execution invoked by the underlying operating system’s timers, potentially causing unexpected latencies. To expose the mentioned impact due to executor differences, in this paper, we present an experimental evaluation of the execution behavior of ROS 2’s schedulable entities, namely callbacks, among the existing versions of the executor. We visualize the differences of callback execution order via simulation, and we create design-level scenarios that impact the execution of periodically scheduled callbacks, negatively. Moreover, we show how such negative impact can be mitigated by using multi-threaded executors. Finally, we illustrate the observed behavior on a real-world centralized multi-agent robot system. Our work aims to raise awareness within the ROS 2 developer community, regarding possible problems of timer blocking, and propose a mitigation solution of the latter.

Planning is a critical function of multi-agent autonomous systems, which includes path finding and task scheduling. Exhaustive search-based methods such as model checking and algorithmic game theory can solve simple instances of multi-agent planning. However, these methods suffer from state-space explosion when the number of agents is large. Learning-based methods can alleviate this problem, but lack a guarantee of correctness of the results. In this paper, we introduce MoCReL, a new version of our previously proposed method that combines model checking with reinforcement learning in solving the planning problem. The approach takes advantage of reinforcement learning to synthesize path plans and task schedules for large numbers of autonomous agents, and of model checking to verify the correctness of the synthesized strategies. Further, MoCReL can compress large strategies into smaller ones that have down to 0.05% of the original sizes, while preserving their correctness, which we show in this paper. MoCReL is integrated into a new version of Uppaal Stratego that supports calling external libraries when running learning and verification of timed games models.

Abstract Path planning and task scheduling are two challenging problems in the design of multiple autonomous agents. Both problems can be solved by the use of exhaustive search techniques such as model checking and algorithmic game theory. However, model checking suffers from the infamous state-space explosion problem that makes it inefficient at solving the problems when the number of agents is large, which is often the case in realistic scenarios. In this paper, we propose a new version of our novel approach called MCRL that integrates model checking and reinforcement learning to alleviate this scalability limitation. We apply this new technique to synthesize path planning and task scheduling strategies for multiple autonomous agents. Our method is capable of handling a larger number of agents if compared to what is feasibly handled by the model-checking technique alone. Additionally, MCRL also guarantees the correctness of the synthesis results via post-verification. The method is implemented in UPPAAL STRATEGO and leverages our tool MALTA for model generation, such that one can use the method with less effort of model construction and higher efficiency of learning than those of the original MCRL. We demonstrate the feasibility of our approach on an industrial case study: an autonomous quarry, and discuss the strengths and weaknesses of the methods.

The paper introduces elements of a service based perspective of a scalable and dynamic automation system architecture. The approach is based on potentially multi-role devices (implementing node management, processing and networking functionalities) hosting a set of services requested by input nodes. In addition, artificial intelligence support is described to provide means of reaching deployment optimality and reliability. Formal approaches are deemed necessary for both verification of the artificial intelligence approach and of the resulting solutions. A model-based design path is complementary considered in order to lead to an increased efficiency in resource utilization, to lowering design efforts, and ensure a formally correct allocation of services, according to system requirements and constraints.

Abstract Many database management systems (DBMS) need to ensure atomicity and isolation of transactions for logical data consistency, as well as to guarantee temporal correctness of the executed transactions. Since the mechanisms for atomicity and isolation may lead to breaching temporal correctness, trade-offs between these properties are often required during the DBMS design. To be able to address this concern, we have previously proposed the pattern-based UPPCART framework, which models the transactions and the DBMS mechanisms as timed automata, and verifies the trade-offs with provable guarantee. However, the manual construction of UPPCART models can require considerable effort and is prone to errors. In this paper, we advance the formal analysis of atomic concurrent real-time transactions with tool-automated construction of UPPCART models. The latter are generated automatically from our previously proposed UTRAN specifications, which are high-level UML-based specifications familiar to designers. To achieve this, we first propose formal definitions for the modeling patterns in UPPCART, as well as for the pattern-based construction of DBMS models, respectively. Based on this, we establish a translational semantics from UTRAN specifications to UPPCART models, to provide the former with a formal semantics relying on timed automata, and develop a tool that implements the automated transformation. We also extend the expressiveness of UTRAN and UPPCART, to incorporate transaction sequences and their timing properties. We demonstrate the specification in UTRAN, automated transformation to UPPCART, and verification of the traded-off properties, via an industrial use case.

The fifth generation of cellular wireless technol- ogy, 5G, bears the promise to transform the future network connectivity by providing seamless, low-latency and reliable interconnections between devices. In this paper, we focus on modeling and analyzing 5G service orchestration that deals with virtual network function placement, resource assignment and traffic routing, which are the building blocks of generating network slices catering to various application requirements. In order to ensure that a particular network slice works as stated by the application's service level agreement, it is essential that the constituent virtual network functions are placed in proper hosts, allocated adequate resources in terms of processing power, memory, bandwidth, and routed such that the constraints of the hosts and the network are met. This is a complex problem to solve if one considers the diverse set of requirements of 5G services. We tackle this problem by proposing a UML-based modeling and analysis framework, called UML5G Service Orchestration Profile, which allows one to describe 5G network slices and service orchestration via a specialized profile, and analyze as-sociated quality-of-service requirements by checking constraints expressed in Object Constraint Language. Our framework allows a designer to model any candidate orchestration scheme for 5G networks and verify if the network function placement, resource assignment, and routing guarantee the application's quality-of-service requirements, at design time. We evaluate the framework on a prototype implementation of an orchestration algorithm that generates a multitude of allocation configurations that we automatically check against requirements formalized in Object Constraint Language. Our contribution facilitates modeling and design-time evaluation of network slicing and service orchestration schemes in 5G-based solutions.

With the ever-increasing size and complexity of the industrial software systems there is an imperative need for an automated, systematic and exhaustive verification of various software artifacts, s ...

Modern cyber-physical systems usually assume a certain degree of autonomy. Such systems, like Ambient Assisted Living systems aimed at assisting elderly people in their daily life, often need to pe ...

Many industrial control systems manage critical data using Database Management Systems (DBMS). The correctness of transactions, especially their atomicity, isolation and temporal correctness, is essential for the dependability of the entire system. Existing methods and techniques, however, either lack the ability to analyze the interplay of these properties, or do not scale well for systems with large amounts of transactions and data, and complex transaction management mechanisms. In this paper, we propose to analyze large scale real-time database systems using statistical model checking. We propose a pattern-based framework, by extending our previous work, to model the real-time DBMS as a network of stochastic timed automata, which can be analyzed by UPPAAL Statistical Model Checker. We present an industrial case study, in which we design a collision avoidance system for multiple autonomous construction vehicles, via concurrency control of a real-time DBMS. The desired properties of the designed system are analyzed using our proposed framework.

Software-to-hardware allocation plays an important role in the development of resource-constrained automotive embedded systems that are required to meet timing, reliability and power requirements. This paper proposes an Integer Linear Programming optimization approach for the allocation of fault-tolerant embedded software applications that are developed using the AUTOSAR standard. The allocation takes into account the timing and reliability requirements of the multirate software applications and the heterogeneity of their execution platforms. The optimization objective is to minimize the total power consumption of the applications that are distributed over multiple computing units. The proposed approach is evaluated using a range of different software applications from the automotive domain, which are generated using the real-world automotive benchmark. The evaluation results indicate that our proposed allocation approach is effective while meeting the timing, reliability, and power requirements of the considered automotive software applications.

Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.

Although atomicity, isolation and temporal correctness are crucial to the dependability of many real-time database-centric systems, the selected assurance mechanism for one property may breach another. Trading off these properties requires to specify and analyze their dependencies, together with the selected supporting mechanisms (abort recovery, concurrency control, and scheduling), which is still insufficiently supported. In this paper, we propose a UML profile, called UTRAN, for specifying atomic concurrent real-time transactions, with explicit support for all three properties and their supporting mechanisms. We also propose a pattern-based modeling framework, called UPPCART, to formalize the transactions and the mechanisms specified in UTRAN, as UPPAAL timed automata. Various mechanisms can be modeled flexibly using our reusable patterns, after which the desired properties can be verified by the UPPAAL model checker. Our techniques facilitate systematic analysis of atomicity, isolation and temporal correctness trade-offs with guarantee, thus contributing to a dependable real-time database system.

The increase in life expectancy and the slumping birth rates across the world result in lengthening the average age of the society. Therefore, we are in need of techniques that will assist the elderly in their daily life, while preventing their social isolation. The recent developments in Ambient Intelligence and Information and Communication Technologies have facilitated a technological revolution in the field of Ambient Assisted Living. At present, there are many technologies on the market that support the independent life of older adults, requiring less assistance from family and caregivers, yet most of them offer isolated services, such as health monitoring, reminders etc, moreover none of current solutions incorporates the integration of various functionalities and user preferences or are formally analyzed for their functionality and quality-of-service attributes, a much needed endeavor in order to ensure safe mitigations of potential critical scenarios. In this paper, we propose a novel architectural solution that integrates necessary functions of an AAL system seamlessly, based on user preferences. To enable the first level of the architecture's analysis, we model our system in Architecture Analysis and Design Language, and carry out its simulation for analyzing the end-to-end data-flow latency, resource budgets and system safety.

CAP Introduction. Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.

Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.

Real-time DataBase Management Systems (RTDBMS) have been considered as a promising means to manage data for data-centric automotive systems. During the design of an RTDBMS, one must carefully trade off data consistency and timeliness, in order to achieve an acceptable level of both properties. Previously, we have proposed a design process called DAGGERS to facilitate a systematic customization of transaction models and decision on the run-time mechanisms. In this paper, we evaluate the applicability of DAGGERS via an industrially relevant case study that aims to design the transaction management for an onboard diagnostic system, which should guarantee both timeliness and data consistency under concurrent access. To achieve this, we apply the pattern-based approach of DAGGERS to formalize the transactions, and derive the appropriate isolation level and concurrency control algorithm guided by model checking. We show by simulation that the implementation of our designed system satisfies the desired timeliness and derived isolation, and demonstrate that DAGGERS helps to customize desired real-time transaction management prior to implementation.

Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.

Dependency analysis techniques are widely used to understand software implementations, and reduce their verification efforts. Recently, architectural languages have started to be integrated in the development of complex embedded systems. Such languages provide early development artifacts, which can be used to specify the structure and functionality of a system, and can be also analyzed in order to provide early information regarding the system's correctness. By performing dependency analysis on architectural languages, crucial dependencies can surface earlier in the life cycle. Once computed, these dependencies can be used to prune the architectural models in an attempt to reduce the early design-stage verification efforts. In this paper, we propose a dependency analysis-based technique that can be applied to prune models in EAST-ADL, an architectural description language tailored to automotive systems development. To achieve correct pruning, we investigate the types of dependencies that can appear in an architectural model, and how these dependencies create dependency chains within the model. Next, we investigate how such dependency chains can be exploited in formal verification in order to reduce the verified state-spaces during model-checking. Assuming a given requirement, our pruning method entails that only the relevant dependency chains are examined during EAST-ADL model-checking against that particular requirement. We validate our analysis results by comparing them to those obtained by applying an analytical approach for end-to-end timing analysis in EAST-ADL models. The methodology is illustrated on a Brake-by-Wire industrial system.

Most industrial embedded systems requirements are specified in natural language, hence they can sometimes be ambiguous and error-prone.Moreover, employing an early-stage model-based incremental system development using multiple levels of abstraction, for instance via architectural languages such as EAST-ADL, calls for different granularity requirements specifications described with abstraction-specific concepts that reflect the respective abstraction level effectively.In this paper, we propose a toolchain for structured requirements specification in the ReSA language, which scales to multiple EAST-ADL levels of abstraction.Furthermore, we introduce a consistency function that is seamlessly integrated into the specification toolchain, for the automatic analysis of requirements logical consistency prior to their temporal logic formalization for full formal verification.The consistency check subsumes two parts: (i) transforming ReSA requirements specification into boolean expressions, and (ii) checking the consistency of the resulting boolean expressions by solving the satisfiability of their conjunction with the Z3 SMT solver.For validation, we apply the ReSA toolchain on an industrial vehicle speed control system, namely the Adjustable Speed Limiter.

Ranging from automation systems and robots to smart grids and electronically coupled vehicle convoys, cyber-physical systems are the result of bringing together two worlds: the physical and the digital. Such a marriage poses a variety of challenges in terms of managing the complexity of the often large numbers of inter-connected devices and services, as well as understanding and solving the emerging technological and IT governance issues. These and other aspects have motivated this panel, aimed at discussing the underlying problems, benefits and risks associated with the distributed intelligence of cyber-physical systems.

Presents a listing of the Symposium organizing committee.

ISO 26262 is the new standard for automotive functional safety. This standard identifies major process steps across a large number of system stages as well as safety-related artifacts required as input and output of these steps. The VeriSpec project intends to identify the main challenges for the adoption of ISO 26262 by the heavy-vehicle industry and to provide useful and industrially relevant "components" (methods, tools etc.) required by the standard. The project work targets two main research goals: (i) requirement formalization support, including a usable front-end for specifying requirements by using patterns, and (ii) formal analysis of realizations in form of architectural models at various levels of abstraction, by model-checking the formal representations of the latter. In this paper, we present the current challenges facing industry and justifying VeriSpec, together with a preliminary roadmap for the research.

Formal methods are mathematically-based techniques for the specification, development and verification of software and hardware systems. The term has been applied to a range of notations, theories and tools. As the recent history shows, there is no doubt that some of these rigorous methods have already had a significant impact on practical applications of computing. Moreover, formal methods continue to incorporate new system design paradigms, in an attempt to expand their applicability. In this spirit, this panel aims at discussing the underlying principles of formal methods that make them contribute to increasing the quality and reliability of a design, as well as showing their relation to practical problems, and their potential for the future.

Designing and developing mission-critical embedded systems is challenging, especially due to additional platform constraints regarding timing and computational resources. The development process of embedded systems should include verification techniques already at the architecture design phase, to provide evidence that a system's architecture fulfills its requirements. The Architecture Analysis and Design Language (AADL) is used to model the system's architecture. Among others, the language contains a Behavior Annex, for describing the behavior of an AADL model, at an abstract level. In this paper, we present a verification tool, called ABV, tailored for AADL models with a behavioral annex. Given an architecture defined in AADL and its behavior specified in the associated language, our tool model-checks the latter against the requirements specified in Computation Tree Logic (CTL). ABV is based on AADL's formal denotational semantics implemented in Standard ML, and is encapsulated into an Eclipse plug-in based on the OSATE platform. The tool has been applied on the Production Cell case study, which is briefly described in the paper.

In this paper, we present a tool-chain for the REMES language, which can be used for the construction and analysis of embedded system behavioral models. The tool-chain consists of the following tools: (i) a REMES editor for modeling behaviors of embedded components, (ii) a REMES simulator to test timing and resource behavior prior to formal analysis, and (iii) an automated transformation from REMES to Priced Timed Automata, needed for formal analysis.

In this paper, we introduce the model REMES for formal modeling and analysis of embedded resources such as storage,energy, communication, and computation. The model is a state-machine based behavioral language with support for hierarchical modeling, resource annotations, continuous time, and notions of explicit entry and exit points that make it suitable for component-based modeling of embedded systems.The analysis of REMES-based systems is centered around a weighted sum in which the variables represent the amounts of consumed resources. We describe a number of important resource related analysis problems, including feasibility, trade-off, and optimal resource-utilization analysis.To formalize these problems and provide a basis for rigorous analysis, we show how to analyze REMES models using the framework of priced timed automata and weighted CTL. To illustrate the approach, we describe a case study in which it has been applied to model and analyze resource usage of a temperature control system.

In the fall of 1968, NATO hosted in Garmisch-Partenkirchen, close to Munich, a conference devoted to the problems of the computer industry that was having a great deal of trouble in producing large and complex programs. The term Software Engineering SE) was not in general use at that time, its adoption for the title of this conference was deliberately provocative. As a result, the conference and its report have played a major role in gaining general acceptance of the term SE.

Presents the introductory welcome message from the conference proceedings.

Provides a listing of current committee members and society officers.

The conflicting requirements of real-time embedded systems, e.g. minimizing memory usage while still ensuring that all deadlines are met at run-time, require rigorous analysis of the system's resource consumption, starting at early design stages. In this paper, we glance through several representative frameworks that model and estimate resource usage of embedded systems, pointing out advantages and limitations. In the end, we describe our own view on how to model and carry out formal analysis of embedded resources, along with developing the system.

Real-time embedded systems typically include concurrent tasks of different priorities with time-dependent operations accessing common resources. In this context, unsynchronized parallel executions may lead to hazard situations caused by e.g., race conditions. To be able to detect such faulty system behaviors before implementation, we introduce a unified model of resource constrained, scheduled real-time system descriptions, in Alur's and Henzinger's rigorous framework of timed reactive modules. We take a component-based design perspective and construct the realtime system model, by refinement, as a composition of realtime periodic preemptible tasks with encoded functionality, and a fixed-priority scheduler, all modeled as timed modules. For the model, we express the notions of race condition and redundant locking, formally, as invariance properties that can be verified by model-checking.

We propose a deductive method for constructing reliable reachability controllers, with application to fault-tolerant discrete systems. Designing the controller reduces to finding a strategy to win specific games defined by sequential angelic and demonic nondeterministic statements. During the game, the plant (the demon) tries to prevent the controller (the angel) from achieving its respective goal, modeled by a special kind of liveness property. We show that the angel has a way to enforce the required property, provided that adequate invariance and termination properties hold. The control strategy is obtained by propagating certain assertions into the angelic statement. We illustrate our method on a data-processing application.

We concentrate on two major aspects of reactive system design: behavior control and modularity. These are studied from a formal point of view, within the framework of action systems. The traditional interleaving paradigm is completed with a new barrier synchronization mechanism. This is achieved by introducing a new parallel composition operator, applicable to both discrete and hybrid models. While offering improvements with respect to control and modularity, the approach uses the correctness preserving mechanisms provided by the underlying reasoning environment.

Continuous action systems (CAS) is a formalism intended for modeling hybrid systems (systems that combine discrete control with continuous behavior), and proving properties about the model within refinement calculus. We use a symbolic manipulation program to build a tool for simulating CAS models by, calculating symbolically the time evolution of the discrete and continuous CAS model functions, as explicit and exact expressions of a continuous time variable. We may then study the time behavior and general properties of the model by plotting these functions with respect to time. For certain models our tool eliminates the need for introducing tolerances into the model structure. The tool is useful for checking that the model behaves correctly, and we can sometimes study the behavior of CAS models with in principle infinite precision.