https://www.mdu.se/

Designers of industrial real-time systems are commonly faced with the problem of complex system modeling and analysis, even if a component-based design paradigm is employed. In this paper, we present a case-study in formal modeling and analysis of a turntable system, for which the components are described in the SaveCCM language. The search for general principles underlying the internal structure of our real-time system has motivated us to propose three modeling patterns of common behaviors of real-time components, which can be instantiated in appropriate design contexts. The benefits of such reusable patterns are shown in the case-study, by allowing us to produce easy-to-read and manageable models for the real-time components of the turntable system. Moreover, we believe that the patterns may pave the way toward a generic pattern-based modeling framework targeting real-time systems in particular.

ProCom is a new component model for real-timeand embedded systems, targeting the domains of vehicularand telecommunication systems. In this paper, we describehow the architectural elements of the ProCom componentmodel have been given a formal semantics. The semantics isgiven in a small but powerful finite state machine formalism,with notions of urgency, timing, and priorities. By definingthe semantics in this way, we (i) provide a rigorous and compactdescription of the modeling elements of ProCom, (ii) setthe ground for formal analysis using other formalisms, and(iii) provide an intuitive and useful description for bothpractitioners and researchers. To illustrate the approach,we exemplify with a number of particularly interestingcases, ranging from ports and services to components andcomponent hierarchies.

The development of embedded systems often requires the use of various models such as requirements specification, architectural (component-based), and deployment models, across different phases. However, there exists little design support for obtaining suitable component-based designs that satisfy specified requirements and timing constraints. In order to provide guided support for the design process of embedded systems, we introduce several component templates, referred as patterns, which we also formally verify against relevant properties. To illustrate the usefulness of the approach, we have applied the proposed patterns to obtain a component-based design of a temperature control system.

It is critical to analyze characteristics of real-time embedded systems, such as timing behavior, early in the development. In the automotive domain, EAST-ADL is a concrete example of the model-based approach for the architectural modeling of real-time systems. The Timing Augmented Description Language v2 (TADL2) allows for the specification of timing constraints on top of EAST-ADL models. In this paper we propose a formal validation & verification methodology for timing behaviors given with TADL2. The formal semantics of the timing constraints is given as a mapping to the Clock Constraint Specification Language (CCSL), a formal language that implements the MARTE Time Model. Based on such a mapping, the validation is carried out by the simulation of TADL2 specifications. The simulation allows for a rapid prototyping of TADL2 specifications. The verification is performed based on a TADL2 mapping to timed automata modeling using the Uppaal model-checker. The whole process is illustrated on a Brake-By-Wire application.

Systematic and formal development approaches for safety- and mission critical systems are of increasing importance. These systems are often implemented as periodically triggered control systems, to ensure deterministic and analyzable timing behavior. However, integrating timing ‘constraints’ in the development process remains a challenging task. For instance, these constraints itself should be formally verified as consistent and feasible with respect to the system design. In this paper, we present a timed automata based validation approach for EAST-ADL timing constraints for periodic control systems. The constraints are specified using CCSL – the Clock Constraint Specification Language,and transformed into timed automata, to enable formal verification with UPPAAL model-checker. The resulting timed automata specification can be simulated and verified for the formal validation of the timing constraints. Further, the transformed specification model can be easily integrated with the actual system design, thus extending verification aspects. The proposed approach is demonstrated using the timing constraints for an Anti-lock Braking System (ABS) example.

In the development of safety-critical embedded systems, the ability to formally analyze system behavior models, based on timing and causality, helps the designer to get insight into the system’s overall timing behavior. To support the design and analysis of real-time embedded systems, the UML modeling profile MARTE provides CCSL – a time model and a clock constraint specification language. On the one hand, CCSL is an expressive language that supports specification of both logical and chronometric constraints associated with MARTE models. On the other hand, semantic frameworks such as Timed Automata provide verification support for real-time systems. To tackle the challenge of verifying CCSL-based system properties, in this paper, we propose a technique for transforming MARTE/CCSL mode behaviors into Timed Automata for model-checking using the UPPAAL tool. This enables verification of both logical and chronometric properties of the system, which has not been possible before. We demonstrate the proposed transformation and verification approach using two relevant examples of real-time embedded systems.

In the development of embedded systems, the formal analysis of system artifacts, such as structural and behavioral models, helps the system engineers to understand the overall functional and timing behavior of the system. In this case study paper, we present our experience in applying formal verification and validation (V&V) techniques, we had earlier proposed, for an industrial wind turbine system (WTS). We demonstrate the complementary benefits of formal verification in the context of existing V&V practices largely based on simulation and testing. We also discuss some modeling trade-offs and challenges we have identified with the case-study, which are worth being emphasized. One issue is related, for instance, to the expressiveness of the system artifacts, in view of the known limitations of rigorous verification, e.g. model-checking, of industrial systems.