Integration of Software Specification Techniques for Applications in Engineering

This contribution is a short introduction into the research area, which was subject of the priority program SoftSpez of the German Research Council (DFG) in the years 1998-2004. Starting with the aims of this priority program, we give an overview of the activities of SoftSpez and the related international workshops INT 2000-2004 and of the results in six different subject areas presented in this volume.

The applicability of the integrated techniques and methods, which are developed within the DFG priority program Software Specifications, is shown by means of two reference case studies, that describe typical systems from engineering point of view. One belongs to the area Production Automation. The characteristic aspects of process automation and the realized systems are focused in the case study, including open and closed loop control, real-time aspects as well as distribution of control functions.

This chapter discusses a number of challenges to be fulfilled and considered regarding software specification for industrial engineering and control software within manufacturing systems. It does not provide an extensive list of detailed functionalities, but rather discusses generic critical success factors. The common thread is the complex interaction between software development and the techno-socio-economic context in which this activity occurs. The software development needs to produce much more sophisticated artefacts in the future, which requires developers to account for factors that could be ignored in the past. In the future, developers need to widen their view. This chapter describes in which ways they need to enlarge their scope.

The definition of a transparent software architecture is one of the key issues in the early development phases for complex distributed and reactive software systems. We show how to derive an architecture systematically for systems with communication models based on broadcasting. Adequate graphical description techniques for capturing interaction requirements and logical component architectures for broadcasting systems are unavailable so far. We introduce an extension to UML’s sequence diagrams to capture broadcasting scenarios. Furthermore, we present methodological steps for constructively deriving structural and behavioral aspects of the architecture under consideration from the captured scenarios.

Today’s manufacturing industry demands flexible and decentralized production control systems to avoid hours of down time of the production line in case of a failure of a single central production control computer or program. Additionally, today’s market forces demand smaller lot sizes and a more flexible mixture of different products manufactured in parallel on one production line. These requirements increase the complexity of the control software. Consequently, sophisticated techniques for the development of such production systems are needed. In this paper we present an overview of our seamless methodology for integrated design, analysis, and validation for such production control systems. We illustrate our approach by an existing material flow system which is a major part of a real production system. We show how our modelling approach is used for simulation facilities, code generation for programmable logic controllers, and maintenance purposes.

Motivated by the wide acceptance of component based technologies in software development, a component concept for software engineering is applied to modeling in the field of production automation. Taking the modeling of a holonic transport system as an example, it is shown, how function blocks in the sense of production automation can be understood as software engineering components. Thus, the advantages of component based modeling with respect to structuring, exchange and reuse can be transferred to systems in production automation.

“Specification” is a very complex concept. This complexity results initially from the questions “What is the purpose of a specification? What is the subject of a specification?” and “Who writes a specification?”, which in turn lead to the questions “What methods and processes are used for specification?”. Answering these questions in detail and finding a definition for the term “specification” that encompasses the full extent and depth of this term represents an enormous academic challenge; it is also of great practical relevance. Because even if analytical deductions can be made from a specification that provide an understanding in retrospect, the actual milestones of a correct and efficient specification are in fact a goal-oriented synthesis of the subject of specification as a unit and its proper functioning in reality.

As domain modelling has been identified as a key issue for putting formal specification techniques into engineering practice, two reference case studies were elaborated within the research programme “Integration of Software Specification Techniques for Applications in Engineering”. One of them, coming from the railway transportation control domain and using an example of a radio based level crossing control system, was developed at the Institute of Traffic Safety and Automation Engineering. A physical railway model demonstrator was designed and developed as a means of comparison and validation for the formal specifications coming from partners involved in the research program.

For developing precise system definitions and for simplifying the evidence of safety, the use of formal methods is highly recommended in the new European CENELEC standards for safe railway systems (EN 50126, EN 50128, DIN EN 61508). But not only in railway sector these methods are difficult to handle and to understand. This contribution introduces a concept for developing precise system definitions based on a notation, which does justice to engineers. A system definition in notation of the Unified Modeling Language (UML) is presented for the reference case study single-track level crossing in radio-based operation. On the basis of this system definition, relevant safety requirements are stated. These safety requirements form the basis for formal checks of the system definition for correctness and safety. A precondition for formal checks is that the safety requirements are specified in a logic language. For that purpose the safety pattern concept is presented, which supports and guides the user in selecting and instantiating the correct formal specification of safety requirements.

In this paper, the authors introduce an extension of UML for the purpose of hybrid systems modeling. The construction uses the profile mechanism of UML 2.0 which is the standard procedure for extending the Unified Modeling Language. The “intuitive semantics” of the syntactic extension is based on the semantics for hierarchic Hybrid Automata, as suggested by Alur et. al. In contrast to Alur’s formalism, HybridUML allows to label transitions not only with conditions and assignments, but also with signals. Furthermore, our approach associates formal semantics by definition of a transformation from HybridUML specifications into programs of a “low-level” language which is both executable in hard real-time and semantically well-defined. When compared to approaches assigning semantics directly to the high-level constructs of a formal specification language, the transformation approach offers two main advantages: First, semantics can be more easily adapted to syntactic extensions by extending the transformation in an appropriate way. Second, all models are automatically executable, since the low-level language is.

We present the Unified Modeling Language (UML) and show how it can be applied to development of a new railway interlocking and signalling system. Using a simplified example of an interlocking system, we demonstrate principles of an object-oriented approach to specifying functional safety requirements. Starting from an informal specification we create a semi-formal specification based on the UML model. Within conclusions we resume advantages of the presented approach resulting from practical experiences gained in the project aimed at development of a new computer-based interlocking system.

This is the introduction to the chapter on the subject area Petri Nets and Related Approaches in Engineering. After a short report on experiences in this subject area during the DFG Priority Program we introduce and survey the papers of this chapter. Furthermore, we indicate that the work done in the subject area provided answers to important questions and – more importantly – helped to identify the state-of-the-art in the field as well as gaps to be filled by further research and development activities.

This article describes our approach for the specification and verification of production automation systems with real-time properties. We focus on the graphical MFERT notation and RT-OCL (Real-Time Object Constraint Language) for the specification of state-oriented real-time properties. RT-OCL is an extension of the Object Constraint Language (OCL) that is part of the Unified Modeling Language (UML). We introduce the formal semantics of RT-OCL based on a formal model of UML Class and State Diagrams and provide a mapping to temporal logics. The applicability of our approach is demonstrated by the case study of a manufacturing system with automated guided vehicles.

The formal technique STOP is a specific application of Coloured Petri Nets [1]. It serves as a methodical specification of operational processes in automation systems. Each concrete specification made by using STOP can be verified with regard to relative completeness and correctness. The present paper introduces the approach and the application domain of STOP as well as its technical characteristics. By discussing experiences made in application of STOP the theoretical introduction of STOP is additionally practically substantiated.

We present an industrial project at Ericsson Telebit A/S where Coloured Petri Nets (CP-nets or CPNs) have been used for the design and specification of an edge router discovery protocol for mobile ad-hoc networks. The Edge Router Discovery Protocol (ERDP) supports an edge router in a stationary core network in assigning network address prefixes to gateways in mobile ad-hoc networks. This paper focuses on how CP-nets and the CPN computer tools have been applied in the development of ERDP. A CPN model has been constructed that constitutes a formal executable specification of ERDP. Simulation and message sequence charts were used for initial investigations of the protocol’s behaviour. Then state space analysis was applied to conduct a formal verification of the key properties of ERDP. Both the modelling, simulation, and subsequent state space analysis helped in identifying several omissions and errors in the design, demonstrating the benefits of using formal modelling and analysis in a protocol design process.

In this paper we summarize syntax and semantics of modules of elementary signal nets and explain how to synthesize the control for discrete event systems modelled by such modules.Signal nets, introduced in [8,9,10,12], are based on Petri net modules which communicate via signals. Two kinds of signals are employed, namely active signals which force occurrence of (enabled) events, and passive signals which enable/prohibit occurring of events. Modelling with such modules appears to be very natural from an engineering perspective. It enables hierarchical structuring and supports the locality principle.Given an uncontrolled system (a plant), modelled by a module of an elementary signal net, and a control specification, given as a regular language representing the desired signal output behavior of this system, we show step-by-step how to automatically synthesize the maximally permissive and nonblocking behavior of the plant respecting the control specification. Finally, we show how to synthesize the controller (as a module of an elementary signal net) forcing the plant to realize the controlled behavior.

Common engineering approaches and modelling approaches from software engineering are brought together. For the domain of process automation, i.e. product and plant automation, an implementation oriented approach for an object oriented software development for heterogeneous distributed systems is introduced. Model elements for control are added to UML as well as small-scale patterns for plant automation. Besides large-scale patterns are introduced as well as implementational models. The adoption of UML regarding applied diagrams and stereotypes for process automation will be introduced and structured components, an idiom for product automation software development, will be compared to other software engineering notations.

The subject area ‘Charts’ groups together those projects that study visual specification formalisms or charts. Visual formalisms promise to support the use of formal methods in the engineering process of (embedded) software systems by being high-level languages that are equipped with a formal semantics in the elementary formalisms like temporal logic or finite state machines.

We describe the semantics of statecharts as implemented in the current version of the Rhapsody tool. In its original 1996 version this was among the first executable semantics for object-oriented statecharts, and many of its fundamentals have been adopted in the Unified Modeling Language (UML). Due to the special challenges of object-oriented behavior, the semantics of statecharts in Rhapsody differs from the original semantics of statecharts in Statemate. Two of the main differences are: (i) in Rhapsody, changes made in a given step are to take effect in the current step and not in the next step; (ii) in Rhapsody, a step can take more than zero time. This paper constitutes the first description of the executable semantics of Rhapsody, highlighting the differences from the Statemate semantics and making an effort to explain the issues clearly but rigorously, including the motivation for some of the design decisions taken.

In this paper, we present an approach to the interactive verification of statecharts. We use STATEMATE statecharts for the formal specification of safety critical systems and Interval Temporal Logic to formalize the proof conditions. To handle infinite data, complex functions and predicates, we use algebraic specifications.Our verification approach is a basis for the aim of the project ForMoSA to put safety analysis techniques on formal grounds. As part of this approach, fault tree analysis (FTA) has been formalized yielding conditions that can be verified using the calculus defined in this paper. Verification conditions resulting from the formal FTA of the radio-based level crossing control have been successfully verified.

The language of Message Sequence Charts (MSC) is a well-established visual formalism which is typically used to capture scenarios in the early stages of system development. But when it comes to rigorous requirements capturing, in particular in the context of formal verification, serious deficiencies emerge: MSCs do not provide means to distinguish mandatory and possible behavior, for example to demand that a communication is required to finally occur.The Live Sequence Chart (LSC) language introduces the distinction between mandatory and possible on the level of the whole chart and for the elements messages, locations, and conditions. Furthermore they provide means to specify the desired activation time by an activation condition or by a whole communication sequence, called pre-chart.We present the current stage of LSC language and a sketch of its formal semantics in terms of Timed Büchi Automata.

Programmable Logic Controllers (PLC) are widely used as device controllers for assembly lines, chemical processes, or power plants. Sequential Function Charts (SFC) form one of the main programming languages for PLCs and, therefore, the correctness of the PLC software implemented as SFCs is crucial for a safe operation of the controlled process. A prerequisite for reasoning about program correctness is a clear understanding of the program semantics. As we show in this work, this is currently not the case for SFCs. Although syntactically specified in the IEC 61131-3 standard, SFCs lack an unambiguous, complete semantic description. We point out a number of problems and explain how these lead to different interpretations in commercial programming environments. To remedy this situation we introduce a parameterized formal semantics for SFCs including many high-level programming features such as parallelism, hierarchy, actions and activity manipulation. Moreover, we show how to extend the semantics to include time, clocks, and timed actions. The presented semantics is general enough to comprise different existing interpretations while at the same time being adjustable to precisely represent each of them.

Over the last two decades the use of software in technical applications has dramatically increased. Almost all real-world systems are now embedded systems consisting of hardware and software components. Just think of modern automobiles; every new car comes equipped with computers that have many tasks in almost all parts of the car: fuel injection rates of the engine, airbags, anti-blocking systems (ABS) for brakes or the anti-theft device are some examples.

This invited paper presents a number of correlated specifications of example railway system problems. They use a variety of partially or fully integrated formal specification. The paper thus represents a mere repository of what we consider interesting case studies.The existence of the Unified Modeling Language [10,67,36,20] has caused, for one reason or another, the research community to try formalise one or another facet of UML. In this paper we report on another way to achieve what UML attempts to achieve: Broadness of application, convenience of notation, and multiplicity of views. Whether these different UML views are unified, integrated, correlated or merely co–located is for others to dispute. We also seek to support multiple views, but are also in no doubt that there must be sound, well defined relations between such views.We thus report on ways and means of integrating formal techniques such as RAISE (RSL) [58,59], Petri Nets [56,62,37,61,41], Message and Live Sequence Charts [42,43,44,64,13], Statecharts [23,24,26,27], RAISE with Timing (TRSL) [18,45,46], and TRSL with Duration Calculus [79,30]. In this way one achieves a firm foundation for combined uses of these formal development techniques, one that can be believably deployed for as wide a spectrum, or even a wider spectrum of software (and hardware) development, as, respectively than UML.

The design of software for distributed production control systems (DPCS) is an error prone task. Ensuring the correctness of the design at the earliest stage possible is a major challenge in any software development process. In this context, formal verification is a very appealing approach in addition to simulation and testing, since it implies an exhaustive exploration of all possible behaviours of a system. In this paper, we present an approach towards model based formal verification for DPCS by means of model checking. The presented work is a part of the ISILEIT project that aims at the development of a seamless methodology for the integrated design, analysis and validation of distributed production control systems.A prerequisite for model based formal verification is the existence of a formal model of the designed system. According to the ISILEIT design methodology a system is specified and modelled using an integrative specification language that combines modeling concepts taken from two different specification languages, namely the UML and the SDL languages. However, supporting formal verification for such a heterogeneous language implies requirements on formal unification and semantic integration of the adopted modeling concepts. In our approach the Abstract State Machines (ASM) formalism represents the formal platform for the unification and semantic integration. We show how the ASMs, in particular the AsmL language, have been successfully applied for creating a rigorous unified semantic model that integrates the semantics of UML State Machines, SDL Block Diagrams and Story Diagrams which form the core of the integrative specification language used in ISILEIT.Besides the integration purpose, the ASMs serve as a basis for the application of model checking techniques. Therefore, the rest of the paper presents the work on adoption of state-of-the-art model checking techniques in order to support model checking of the ASM (AsmL) models.

In the ForMoSA project [18] an integrated approach for safety analysis of critical, embedded systems has been developed. The approach brings together the best of engineering practice, formal methods and mathematics: traditional safety analysis, temporal logics and verification, and statistics and optimization.These three orthogonal techniques cover three different aspects of safety: fault tolerance, functional correctness and quantitative analysis. The ForMoSA approach combines these techniques to answer the safety relevant questions in a structured and formal way. Furthermore, the tight combination of methods from different analysis domains yields results which can not be produced by any single technique.The methodology was applied in form of case studies to different industrial domains. One of them is the height control of the Elbtunnel in Hamburg [17] from the domain of electronic traffic control, which we present as an illustrating example.

This paper presents how a model-based development process can be enhanced by the combination of using Live Sequence Charts (LSC) as the formal language to describe interactions together with automatic formal verification techniques that decide whether communication sequences are exhibitable or adhered to by the system. We exemplify our approach on the V-model, a widely used development process, considering a (Statemate) statecharts design of the reference case study “Funkfahrbetrieb” (FFB) and discuss potential assets and drawbacks. We sketch a set of best practices on the use of LSC features and emphasise the possibilities for re-use of LSCs in the different activities of the development process. To give evidence for feasibility of automatic formal verification of LSCs, as well as its limitations, we present our approaches to the verification of possible and mandatory LSC requirements on Statemate models. We report experimental results we have obtained from formal verification of the FFB and briefly discuss the treatment of Statemate’s different notions of time.

Programmable Logic Controllers (PLC) are widespread in the manufacturing and processing industries to realize sequential procedures and to avoid safety-critical states. For the specification and the implementation of PLC programs, the graphical and hierarchical language Sequential Function Charts (SFC) is increasingly used in industry. To investigate the correctness of SFC programs with respect to a given set of requirements, this contribution advocates the use of formal verification. We present two different approaches to convert SFC programs algorithmically into automata models that are amenable to model checking. While the first approach translates untimed SFC into the input language of the tool Cadence SMV, the second converts timed SFC into timed automata which can be analyzed by the tool Uppaal. For different processing system examples, we illustrate the complete verification procedure consisting of controller specification, model transformation, integration of dynamic plant models, and identifying errors in the control program by model checking.

This paper presents the real-time model checker RAVEN and related theoretical background. RAVEN augments the efficiency of traditional symbolic model checking with possibilities to describe real-time systems. These extensions rely on multi-terminal binary decision diagrams to represent time delays and time intervals. The temporal logic CCTL is used to specify properties with time constraints. Another noteworthy feature of our model checker is its ability to compose a system description out of communicating modules, so called I/O-interval structures. This modular approach to system description alleviates the omnipresent state explosion problem common to all model checking tools.The case study of a holonic material transport system demonstrates how such a production automation system can be modeled in our system. We devise a detailed model of all components present in the described system. This model serves as basis for checking real-time properties of the system as well as for computing key properties like system latencies and minimal response times. A translation of the original model also allows application of another time bounded property checker for verification of the holonic production system. Finally, we present an approach combining simulation and formal verification that operates on the same system model. It enables verification of larger designs at the cost of reduced coverage. Only critical states detected during simulation runs are further subjected to exhaustive model checking. We contrast the runtimes and results of our different approaches.

Integration is a necessary activity in each software development process. Within a model-based approach also the models that are used must be integrated. Model integration has two dimensions: On the one hand, the model components that result from the decomposition of the system under consideration have to be put together. On the other hand, different views onto the system are distinguished and modelled separately in order to decrease the complexity of the development process; the according models also must be brought together again.Integration models are meta-level definitions of model integration methods. Ideally they can be instantiated with arbitrary kinds of models and modelling languages, which then yields an integration method for these models. In this introduction integration modelling is put into perspective; integration models are presented in the following contributions.

The specification and modelling of reasonably large software systems is usually a complex task that involves the description of several aspects or dimensions that are not easily described by means of a single specification technique or formalism. However, an obvious problem in this context is to know how can we be sure that these specifications are consistent and really model the system that we want to design. A second problem is how to verify or prove properties about these systems. In this paper, we will provide a formal framework that will allow us to reason about heterogeneous specifications and we will present some results concerning these two problems.

Complex systems have many heterogeneous aspects, which can be specified comprehensibly and adequately by viewpoint specification techniques dealing only with a suitable subset of these aspects. A methodology for the formal integration of collections of such viewpoint specification techniques is introduced and applied to object-oriented systems. As a main result, it is shown, how the semantical consistency of viewpoint specification techniques can be checked in this framework.