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.

In the development of embedded software, modeling languages used within or across development phases e.g., requirements, specification, design, etc are based on different paradigms and an approach for relating these is needed. In this paper, we present a formal framework for relating specification and design models of embedded systems. We have chosen UML statemachines as specification models and ProCom component language for design models. While the specification is event-driven, the design is based on time triggering and data ow. To relate these abstractions, through the execution trajectories of corresponding models, formal semantics for both kinds of models and a set of inference rules are defined. The approach is applied on an autonomous truck case-study.

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.