Abstract With the increasing complexity of dynamic concurrent systems, a phase of formal specification and formal verification is needed. UML state machines are widely used to specify dynamic systems behaviours. However, the official semantics of UML is described in a semi-formal manner, which renders the formal verification of complex systems delicate. In this paper, we propose a formalisation of UML state machines using coloured Petri nets. We consider in particular concurrent aspects (orthogonal regions, forks, joins, variables), the hierarchy induced by composite states and their associated activities, external, local or inter-level transitions, entry/exit/do behaviours, transition priorities, and shallow history pseudostates. We use a CD player as a motivating example, and run various verifications using CPN Tools.

This paper deals with a formal approach for the detection of situations in the context of complex event processing, which is a technique particularly employed in the aerospace field. Indeed, aerospace systems generally involve numerous interacting agents, to each of which are associated various possible events, thus yielding a huge flow of events. A common issue when dealing with the safety of such systems consists in being able to detect in this flow certain event correlations, from which one may then deduce that the system is in a particular (often critical or hazardous) state. This work is based on a situation description language called chronicles, and provides for it a formal recognition model based on coloured Petri nets. A two-layer compositional model is provided: a concurrent, nondeterministic recognition model for each chronicle construct, together with additional control structures allowing to overview the recognition treatments performed on the event flow.

This paper focuses on an application of formal methods: behavior detection, where a formal language is used to describe behaviors within a system, together with formal recognition rules used to detect these described behaviors within an event flow resulting from the operation of the system. This formal approach is very interesting for aerospace system studies: these generally involve numerous interacting agents and are thus very complex. Since actual systems are too expensive or too critical to be directly studied, they require simulations. Formal behavior detection is a convenient method allowing, in a non-intrusive way, to evidence within a very complex simulation the data necessary to understand finely the behavior of some agents. This data may be used to evidence integration problems in the simulation, or to exploit its results. We present an application where formal behavior detection has proven to be very beneficial, and the formal framework used, namely a description language called chronicles and an operational recognition model provided by a modular coloured Petri net semantics, which we prove to be adequate with the set definition of the recognition notion.

Chronicles are used to describe behaviours, e.g. when (un) desired behaviours should be detected within an event flow, for instance in aerospace system studies. In this paper we first introduce a language to describe chronicles and event related notions, before defining a denotational semantics of a chronicle recognition within an event flow. We present an operational semantics of chronicle recognitions using coloured Petri nets. This modelling is designed to be modular and composible, and to retrieve information on which events in the flow contributed to the chronicle recognition. We prove on some constructs of the chronicle language that our modelling of the recognition using coloured Petri nets yields the expected recognition.

In this paper, we present a pattern-based software development process using problem frames and corresponding architectural patterns. In decomposing a complex problem into simple subproblems, the relationships between the sub-problems are recorded explicitly. Based on this information, we give guidelines on how to derive the software architecture for the overall problem from the software architectures of the simple subproblems.

Formal specifications are now widely accepted in software development. Recently, the need for a separation of concerns with reference to static and dynamic aspects appeared. Furthermore, in order to be able to design complex architectures and communication patterns, we need a structured approach which allows us to decompose a system into subparts and to recompose it from them. Finally, a notion of formal reusable component which is suitable to describe both functional and dynamic aspects is also required. This paper presents the Korrigan model. It allows one to specify in a uniform and structured way both datatypes and behaviours using Symbolic Transition Systems and algebraic specifications. We demonstrate its ability to describe reusable components in a formal way with well defined interfaces. We also demonstrate that Korrigan is relevant to describe the architecture and communication schemes of systems that may present a complex structure.