MoDELS'09 ACES-MB Workshop Proceedings Formal Design Models for Distributed Embedded Control Systems Christo Angelov, Krzysztof Sierszecki, Yu Guo Mads Clausen Institute for Product Innovation University of Southern Denmark Alsion 2, 6400 Soenderborg, Denmark {angelov, ksi, guo}@mci.sdu.dk Abstract. The paper presents a formal specification of the software design models used in COMDES-II – a component-based framework for distributed control systems, featuring open architecture and predictable operation under hard real-time constraints. In this framework, an application is modelled as a network of distributed embedded actors that communicate transparently by exchanging labeled messages (signals), independent of their allocation on network nodes. Actors are configured from prefabricated executable components such as modal function blocks controlled by a master state machine, whereby actor structure is specified by a data flow model (function block network). Accordingly, actor behaviour is specified by composite functions representing signal transformations - from input to output signals, and system behaviour - by actor-level composite functions representing the overall sequence of computation – from system input to system output signals. Input and output signals are exchanged with the controlled plant at precisely specified time instants in accordance with the concept of Distributed Timed Multitasking, resulting in the elimination of transaction I/O jitter. System operation is ultimately described by a clocked synchronous model of computation featuring communicating actors, atomic (zero-time) execution of input and output actions and constant, non-zero execution time of system reactions. Keywords: distributed control systems, component-based design of embedded software, domain-specific frameworks, correct-by-construction systems 1 Introduction Nowadays, embedded software development is still dominated by conventional design methods and manual coding techniques. However, these are not able to cope with continuously growing demands for high quality of service, reduced development and operational costs, reduced time to market, as well as ever growing demands for software safety and dependability. In particular, software safety is severely affected by design errors that are typical for informal design methods, as well as implementation errors that are introduced during the process of manual coding. Denver, CO, USA, October 6, 2009 43 MoDELS'09 ACES-MB Workshop Proceedings This situation has stimulated the development of new software design methods based on formal design models (frameworks) specifying system structure and behaviour, which can be verified and validated before the generation of the program code [1, 2]. Furthermore, model-driven development can be combined with component-based design, whereby design models are implemented by means of reusable and reconfigurable components. Thus, embedded applications can be configured using repositories of prefabricated and validated components (rather than programmed), whereby the configuration specification is stored in data structures containing relevant information such as component parameters, input/output connections, execution sequences, etc. Hence, it is possible to reconfigure applications by updating data structures rather than reprogramming and reloading the entire application. The main problem that has to be addressed with this method is to develop a comprehensive, yet intuitive and open framework for embedded systems. There are a considerable number of frameworks developed in the traditional Software Engineering domain that employ components with operational interfaces as well as various types of port-based objects, e.g. actor frameworks [4-8]. However, it can be argued that the architecture of the framework (i.e. models used to specify component functionality, interfacing and interaction) should be derived from areas such as Control Engineering and System Science, taking into account that modern embedded systems are predominantly control and monitoring systems. This approach has been used for some time with industrial control systems, whose software is built from component objects (function blocks) that implement standard application functions and interact by exchanging signals. Accordingly, function blocks are „softwired‟ into function block networks that are mapped onto real-time control tasks, e.g. standards IEC 61131-3 [10] and IEC 61499 [11]. Unfortunately, this is a relatively low-level approach, which is inadequate for modern embedded applications. These vary from simple controllers to highly complex, time-critical and distributed systems featuring autonomous subsystems with concurrently running activities (tasks) that have to interact with one another within various types of distributed transactions. The above standards do not provide modeling techniques and component definitions at this level and do not define concurrency, whereby the mapping of function block networks on real-time tasks, as well as task scheduling and interaction are considered implementation details that are not a part of the standard. In order to overcome the above problems, the Control Engineering models must be augmented with concepts and techniques developed in the Computer Science domain (concurrency, scheduling, communication, state machines, etc.), as advocated by leading experts in the area of Embedded Software Design, e.g. [2], [3]. The resulting framework must support compositionality and scalability through a well-defined hierarchy of reusable and reconfigurable components, including both actors and function blocks. On the other hand, it has to adequately specify system behaviour for a broad range of sequential, continuous and hybrid control applications. These guidelines have been instrumental in developing the framework COMDES-II [13]. This is a domain-specific framework for time-critical distributed control applications, featuring a hierarchical component model as well as transparent signal- based communication at all levels of specification. In COMDES-II, an embedded Denver, CO, USA, October 6, 2009 44 MoDELS'09 ACES-MB Workshop Proceedings application is composed from actors, which are configured from prefabricated function blocks. This is an intuitive and simple model that is easy to use and understand by application experts, i.e. control engineers. An informal description of the above component models is given elsewhere [13]. This paper presents a formal specification of COMDES-II design models focusing on two interrelated aspects, i.e. system structure and behaviour. It is organized as follows: Section 2 presents a top-down specification of system structure in terms of data flow models describing actors and actor interactions, as well the internal structure of actors, which are composed of prefabricated function blocks. Section 3 presents a bottom-up specification of system behaviour starting with function block behaviour, followed by actor behaviour and finally - system behaviour. These are defined as composite functions specifying signal transformations - from input to output signals - of function blocks, actors and the system itself, respectively. Section 4 presents related research. The concluding section summarizes the main features of the framework and their implications for a software development process aimed at designing systems that are correct by construction. 2 Specification of System Structure 2.1 COMDES-II Design Models - an Introduction In COMDES-II, an embedded system is conceived as a composition of active objects (actors) that communicate via labelled state messages (signals) encapsulating process variables, such as speed, pressure, temperature, etc. Communication is transparent, i.e. independent of the allocation of actors on network nodes. Accordingly, the system can be modelled by an actor network specifying constituent actors and the signals exchanged between them (see e.g. Fig. 1). Visualization Unit Command Entry OStationManualVoltage OStationParameters OStationSpeed OStationMode Sensor Controller Speed Voltage Pulses Sensor Controller Actuator Voltage Fig. 1. COMDES-II actor network – an example: the DC Motor Control System An actor is modelled as an integrated circuit consisting of a signal-processing block, which is mapped onto a non-blocking (basic) task, as well as input and output signal drivers that are used to exchange signals with other actors and the outside world (see Fig. 2). Actor tasks are configured from function blocks (FBs) and are modelled by function block networks. A function block is a reusable executable component that Denver, CO, USA, October 6, 2009 45 MoDELS'09 ACES-MB Workshop Proceedings may have multiple instances within a given configuration. There are four kinds of function block: basic, composite, state machine and modal function blocks that can be used to implement a broad range of sequential, continuous and hybrid applications. Input signal drivers Signal processing block (task) Output signal drivers OStationMode 1 mode 1 manual OStationManualVoltage 1 voltage 2 Digital SensorSpeed 1 realRPM 3 1 voltage 1 ControllerVoltage control OStationSpeed 1 setRPM 4 Local signals OStationParameters 1 PIDParam 5 Fig. 2. COMDES-II Controller actor Basic function blocks have simple stateless behaviour, which is specified by functions defining signal transformations - from input signals to output signals (e.g. a PID controller function block). Complex stateful behaviour is implemented with modal function blocks (MFBs). These may be viewed as a generalization of stateless function blocks: a MFB has a number of operational modes where each mode encapsulates one or more FB instances used to execute a control action associated with that mode. A modal function block receives indication of current mode from a supervisory state machine (SSM), whereby it executes the corresponding control action, in the context of a continuous or sequential control actor, e.g. manual/automatic control of DC motor rotation speed (see Fig. 3). A function block network may be encapsulated into a composite function block, which can be subsequently reused as an integral component. 1 mode 1 3 realRPM 2 SSM 1 mode 4 setRPM 3 1 2 MFB 1 voltage 1 3 2 manual voltage 4 5 PIDParam 5 Fig. 3. The Digital control task composed of state machine and modal function blocks Signal drivers are a special class of component - these are wrappers providing an interface to the system operational environment by executing kernel- or hardware- dependent functions. Specifically, signal drivers can invoke kernel primitives to transparently broadcast and receive signals, independent of the allocation of sender and receiver actors on network nodes [14]. A detailed informal description of the above component models is given elsewhere [13]. The following discussion presents a formal specification of COMDES-II components and component configurations. The latter takes into account the two levels Denver, CO, USA, October 6, 2009 46 MoDELS'09 ACES-MB Workshop Proceedings of the framework, i.e. system and actor levels, which are treated in a top-down fashion. At the top level, the system is described as an actor network - a data flow model involving system actors and the global signals exchanged between them, as well as a definition of the signals in terms of identifiers and constituent signal variables. At the next level, each system actor is described by a function block network, i.e. a data flow model involving constituent function blocks and the local signals exchanged. 2.2 Distributed Control System Specification A distributed embedded control system (ECS) is modelled as an actor network: ECS = < A, S, C > , (1) where A is the set of system actors, S is the set of system signals and C is the set of channels used to exchange signals between actors. The set of system actors A consists of environment actors Aenv modelling the plant, and control actors Acon operating in a distributed system environment: A = Aenv Acon . (2) The set of system signals S can be represented as: S = Sin Scom Sout , (3) where Sin is the subset of physical input signals, Scom is the subset of signals (messages) exchanged over the communication network, and Sout is the set of output physical signals. Furthermore, si S: si = < Idi, Vi >, where Idi is a signal identifier and Vi is a set of signal variables defined in terms of variable names and the corresponding data types: Vi = { < si1: typei1>, < si2: typei2>, … , } , (4) e.g. signal OStationParameters consisting of PID parameters, such as proportional, integral and derivative gain values (see Fig. 2). The communication relationship between actors is specified in terms of channels that are defined by a source - signal - destination relation: C A S 2A , (5) e.g. one of the channels depicted in Fig. 1, which is specified by the tuple < Sensor, Sensor_Speed, {Controller, Vizualization_Unit} > . In an actual implementation, control actors will be allocated to network nodes, and channels – to the network communication channel and physical I/O channels. The subsequent discussion assumes a real-time network with predictable message latency, such as CAN, which has been used for the experimental validation of COMDES-II. A system control actor can be defined as: acon = < X , Lin, NFB, Lout, Y > , (6) where: X is the set of input signals received by the actor, X S, Lin is an input signal latch, NFB is a signal-processing network of function blocks, Lout is an output signal latch and Y is a set of output signals generated by the actor, Y S. Denver, CO, USA, October 6, 2009 47 MoDELS'09 ACES-MB Workshop Proceedings The input latch is used to receive input signals and decompose them into input signal variables constituting the set V, which may be viewed as local signals that are processed by the function block network. The latter computes output variables constituting the set W, which are used to compose the output signals generated by the output latch (see e.g. Figs. 2 and 3). The I/O latches are composed of communication objects called signal drivers, denoted as Din and Dout. In particular: Lin = { Dini }; Dini : sini Vi , Vi V, (7) Lout = { Douti }; Douti : Wi souti , Wi W, where Vi and Wi denote the constituent variables of the corresponding I/O signals sini and souti , respectively. The I/O latches are activated at the release and deadline instants of the actor task. This is a basic (non-blocking) task, whose internal structure is specified as a function block network performing the transformation of input signal variables into output signal variables: V W. The FB network is modelled by an acyclic data flow graph (see e.g. Fig. 3), which can be defined as follows: NFB = < B, Z, Con > , (8) where B is a set of function blocks (FBs), Z is a set of FB network variables and Con is the set of FB network connections. A function block performs the signal transformation X Y, where X is the set of FB input variables, X Z, and Y is the set of FB output variables, Y Z. Specifically, a function block can be defined as: FB = < X, Y, P, F > , (9) where X, Y and P denote input, output and persistent variables, respectively and F is a set of functions. Input variables X are generated by input drivers or other function blocks, X Z. These are used together with persistent variables to compute output variables Y, Y Z. Persistent variables P represent the internal state of the function block, which is retained from one execution to the next, e.g. various types of controllers, filters, etc. [10]. Simple function blocks may not have internal state, e.g. arithmetic function blocks, comparators. Output variables are computed by functions f F that are defined as y = f(x, p), where y Y, x X and p P. The variables constituting the set Z may be viewed as local signals associated with the function block network: Z=V I W, (10) where the input signal variables V are generated by input drivers and processed by function blocks; internal variables I are generated and processed by function blocks; output signal variables W are generated by function blocks and used by output drivers to compose output signals (see e.g. Fig. 3). FB network connections are used to wire function blocks with input and output signal drivers, and with each other. The corresponding set can be specified as a union Denver, CO, USA, October 6, 2009 48 MoDELS'09 ACES-MB Workshop Proceedings of subsets denoting input, internal and output connections: Con = Conin Conint Conout . These are defined as source - local signal - destination relations as follows: Conin Lin V B, Conint B I B, (11) Conout B W Lout , e.g. the connection represented by the tuple < SSM, mode, MFB > shown in Fig. 3. 3 Specification of System Behaviour 3.1 COMDES-II Model of Computation – an Introduction System operation is specified in terms of distributed transactions executed in accordance with a model of computation known as Distributed Timed Multitasking [12, 13], which is presently supported by the distributed real-time kernel HARTEXμ [14]. The distributed transaction involves a number of actors that execute transaction phases by invoking sequences of function blocks within the corresponding actor tasks. Actors interact with each other by exchanging labelled state messages (signals) using dedicated communication objects (signal drivers) that provide for transparent one-to- many communication between the actors involved. Distributed Timed Multitasking (DTM) combines the concepts of Timed Multitasking [5] and transparent signal-based communication. With this model, it is assumed that signal drivers are short pieces of code that are executed atomically in logically zero time at precisely specified time instants, which is typical for control applications. Specifically, input signal drivers are executed when the actor task is released, and output drivers - when the task deadline arrives or when the task comes to an end, if it has no deadline (see Fig. 4). Consequently, task I/O jitter is effectively eliminated as long as the task comes to an end before its deadline. Actor task release event Deadline preemption Input drivers Output drivers task jitter Input signals Output signals Fig. 4. Actor execution under Distributed Timed Multitasking Jitter-free operation can be extended to distributed systems, e.g. a phased-aligned transaction involving the actors Sensor (S), Controller (C) and Actuator (A) from Fig. 1, which are triggered by a periodic timing event, such as a synchronization (sync) message denoting the initial instant of the transaction period (T), with deadline D ≤ T Denver, CO, USA, October 6, 2009 49 MoDELS'09 ACES-MB Workshop Proceedings (see Fig. 5). In this case, input and output signals are generated at transaction start and deadline instants, resulting in the elimination of transaction I/O jitter. OStationSync deadline event sensor s→c message arrival event controller c→a actuator tik tok tik+1 tok+1 I/O D (D ≤ T) T Fig. 5. Jitter-free execution of distributed transactions The following discussion presents a formal specification of system operation, taking into account the adopted model of computation and the model of system structure developed in the preceding section. 3.2 Specification of Function Block Behaviour Function block operation is specified with simple and/or composite functions from FB input variables x(k) to FB output variables y(k), x X, y Y, assuming periodic execution of system actors and constituent function blocks, which are invoked at time instants kT, k = 1, 2, …... , where T is the execution period of the host actor. Basic function blocks implement standard signal-processing functions, such as: y(k) = f(x(k)) - with simple FBs implementing various kinds of (12) mathematical operations, comparators, etc. y(k) = f(x(k), p(k-1), p(k-2), … p(k-l)) - with FBs having persistent state, (13) where the state is defined in terms of one or more persistent variables p(k-1), p(k-2), …., p(k-l), retained from previous periods 1, 2 …, l and updated during each period (as specified by the concrete FB algorithm, e.g. the discrete-time versions of filters, various control algorithms, etc. [10]). A composite function block (CFB) encapsulates a FB network whose behaviour is described with one or more functions such as y(k) = f(x(k)) , where f is a composite function specifying the transformation of signals from CFB inputs to CFB outputs, which is defined in terms of the functions executed by the constituent function blocks. Assuming that the CFB encapsulates a sequence of r function blocks, this function can be represented as: f = fr ◦ fr-1 ◦ .... ◦ f1 , or using another notation: y(k) = fr ( fr-1 ( ... ( f1(x(k)))...)) (14) Denver, CO, USA, October 6, 2009 50 MoDELS'09 ACES-MB Workshop Proceedings In the general case, this function will have a different expression for each particular configuration of the FB network, which has to be always modelled by an acyclic data flow diagram. However, cycles are allowed at actor level but these are effectively broken by one-period delays due to the adopted clocked synchronous model of computation (see below). The supervisory state machine (SSM) implements the reactive aspect of actor behaviour, in separation from the transformational (signal processing) aspect, which is delegated to the modal function block. The SSM generates two output signals - m and u, meaning mode and mode-updated, which are specified by the corresponding functions: m(k) = f (m(k-1), e(k), pr(e(k)) - a mode transition function, and u(k) - a Boolean function, which is defined as follows: (15) u(k) = true when m(k) ≠ m(k-1), i.e. when a mode transition has taken place, u(k) = false when m(k) = m(k-1), and no transition has taken place. In the above expression e(k) denotes a transition trigger, i.e. an event specified as a Boolean expression involving binary input signals that are present at time kT, T is the period of the host actor, and pr(k) is the priority of the event triggering the transition from m(k-1) to m(k). The modal function block (MFB) implements the signal processing aspect of actor behaviour by executing constituent function blocks within the corresponding modes of operation. These compute control signals yi, i = 1, 2, …, r, by invoking signal transformation functions f1, f2, …., fr – from input to output signals. Subsets of these functions are selected for execution, depending on the mode and mode-updated input signals indicated by the state machine function block, such that: yi Ap , yi(k) = fi(x(k)) , and yi Aq, q p, yi(k) = yi(k-1) - when m(k) = p and u(k) = true; (16) yi , yi(k) = yi(k-1) - when u(k) = false , where Ap denotes the control action, i.e. the subset of control signals generated in mode p, and fi is the function executed by the corresponding function block(s) in order to generate the signal yi, yi Ap. For instance, the control signal voltage of Fig.3 will be generated by a PID function block if mode has been updated to automatic. The composition of supervisory state machine and modal function block operates as a periodically executed event-driven state machine whose operational semantics and implementation are presented in [15]. This state machine is invoked within a periodically executing host actor but a state transition takes place only when the corresponding transition trigger is present, much in the same way as event-driven state machines triggered by external interrupts. 3.3 Specification of Actor Behaviour Actors generate reactions to execution triggering events in the form: e Ye , (17) Denver, CO, USA, October 6, 2009 51 MoDELS'09 ACES-MB Workshop Proceedings where Ye Y, Ye being the set of output signals generated by the actor in response to the execution trigger e. The latter may be a local timing event ↑(kT), a global timing event ↑sync(kT) generated by a periodic synchronization message or an external event ↑xtrigger , where xtrigger is one of the actor input signals (e.g. a message arrival event)1. Actor output signals y Y are specified by functions of input signals x X that are latched by input drivers at the time of input tin. With periodic actors triggered by local or global timing events tin = kT, k = 0, 1, 2, … Output signals are composed of output signal variables generated by the actor FB network, which has a zero logical execution time (LET). Hence, the output signal variables are logically related to the input time instant kT: w(k) = φ(v(k)) , (18) where φ is a composite function – from input signal variables v V to output signal variables w W that constitute actor input signals x and output signals y, respectively. With actors having purely transformational behaviour, φ can be defined like a CFB function, e.g.: φ = fr ◦ fr-1 ◦ ….. ◦ f1 , (19) where fi are basic and/or composite signal-transformation functions executed by constituent function blocks, i = 1, 2, …, r. With complex actors built from supervisory state machines coupled to modal function blocks, each mode generates certain control signals specified by the corresponding functions, for example: w1(k) = φ1 (v(k)) - generated in mode 1 w2(k) = φ2 (v(k)) - generated in mode 2 (20) ............................. ws(k) = φs (v(k)) - generated in mode s In this case, for each φi , φi = fi ◦ m , where m is the mode transition function of the SSM function block and fi(v(k)) is the signal transformation function executed by the modal function block when the supervisory state machine has indicated that m(k) = i. In the general case: φi = fi ◦ m ◦ g , (21) where g denotes a pre-processing function. The latter is executed by a pre-processing (basic or composite) function block, generating a transition-trigger signal for the supervisory state machine (e.g. various types of arithmetic, comparators, counters, etc.) The output variables generated by the actor task are used to compose output signals, which are latched into the output drivers at the time of output: y(tout) = φ(x(tin)) , tout = tin+ D = kT + D, k = 0, 1, 2, … ; 0 ≤ D ≤ T , (22) Hence: y(kT + D) = φ(x(kT)) , (23) 1 Bold symbols denote actor-level events and input/output signals. Denver, CO, USA, October 6, 2009 52 MoDELS'09 ACES-MB Workshop Proceedings and the actor as a whole has a clocked synchronous semantics [19], chracterized by a non-zero logical execution time (LET). In the special case of actor without deadline, it is assumed that D = 0, and tin = tout = kT. Hence: y(k) = φ(x(k)), and the actor has a perfect synchronous semantics (zero LET). This is the case with intermediate actors of phase-aligned transactions, where the deadline is usually associated with the last actor, which has to generate the control signal at the transaction deadline instant (see next section). 3.4 Specification of System Behaviour System operation is specified in terms of distributed transactions, such as the transaction shown in Fig. 5, assuming: 1) Periodic phase-aligned transactions involving non-blocking basic tasks, such as the one shown in Fig. 5, which are typical for distributed control applications [18]; 2) Non-blocking signal-based communication; 3) Distributed Timed Multitasking, which is an extension of Timed Multitasking for distributed transactions. Under these assumptions, a periodic phase-aligned transaction with a period Ttrans can be represented as a sequence of transaction phases, involving a number of actors, which are executed in response to a global timing event ↑sync(kTtrans) represented by the arrival of a synchronisation (sync) message generated by a sync master node: ↑sync(kTtrans) y1 ; y1 = φ1 (x1) , ↑x2 y2 ; y2 = φ2 (x2) , (24) ..................... ↑xn yn ; yn = φn (xn) , where: x1 = xin , x2 = y1, x3 = y2 ,…, xn = yn-1, yn = yout . Hence, transaction execution can be modelled with a composite function: Φ = φn ◦ φn-1 ◦ ….. ◦ φ1 , (25) where φi is the function implemented by the i-th actor, i = 1, 2, …., n. Taking into account Distributed Timed Multitasking, transaction execution can be represented as a transformation from input signals xin(tin) to output signals yout(tout), where tin and tout are determined by the transaction period Ttrans and deadline Dtrans : ↑sync(kTtrans) yout , (26) yout (kTtrans + Dtrans) = Φ(xin (kTtrans)); Dtrans ≤ Ttrans . For the particular example illustrated by Figures 1 and 5, the behaviour of the control system can be represented in the form: Voltage(kTtrans + Dtrans) = Φ(pulses(kTtrans)), Φ = φactuator ◦ φcontroller ◦ φsensor . In the general case, the distributed system may consist of multiple subsystems executing distributed transactions with different rates of activation (multi-rate system), e.g. a multi-loop distributed control system. Accordingly, subsystem actors are allocated onto network nodes, and subsystem channels – onto the physical Denver, CO, USA, October 6, 2009 53 MoDELS'09 ACES-MB Workshop Proceedings communication channel(s). This raises the issue of concurrent execution of transaction tasks/communications within the corresponding operational domains. Following the adopted model of computation (Fig. 4), actor tasks are executed in a dynamic priority-driven scheduling environment provided by node-resident kernels, which are instances of the HARTEXμ timed multitasking kernel [14]. Communication takes place in a real-time network supporting predictable interactions, such as CAN. Transparent signal-based communication is supported by a dedicated protocol provided by the HARTEXμ kernel. With this protocol, signal drivers are executed atomically at precisely specified time instants that are fixed on the time axis. This makes it possible to eliminate the undesirable effects of task preemption and network communication, i.e. transaction I/O jitter, as long as transaction (end-to-end) response times are less than the corresponding end-to-end deadlines. This requirement can be checked using response time analysis developed for distributed real-time systems, e.g. the analysis method and tool presented in [18]. 4 Related research COMDES-II is a follow-on version of COMDES-I [12]. It employs an actor-based system model, whereby actors are conceived as units of concurrency as well as functionality (e.g., sensor, controller, actuator, etc.), whereas in the previous version a system is composed from function units encapsulating multiple threads of control. It also incorporates a different, i.e. composite state machine model emphasizing the separation of reactive and transformational (signal-processing) behaviour. In COMDES-II, system operation is described by the Distributed Timed Multitasking (DTM) model of computation, which has been inspired by the original Timed Multitasking model [5] and is similar to the LET model adopted in the xGiotto language [6]. However, both of these models use port-based communication between actors, whereas DTM employs broadcast communication with labeled state messages (signals). This solution rules out artifacts such as ports, message queues, mailboxes, operational interfaces, etc., and provides for transparent interactions that are independent of the allocation of the actors on network nodes. Furthermore, the above frameworks use flat actor models with actors programmed in a conventional fashion, whereas COMDES-II actors are configured from prefabricated executable components – function blocks. The adopted communication mechanism is characterized by complete separation of computation and communication, as recommended in [9], since signal drivers are executed in separation from actor tasks and from each other. That is not the case with port-based objects, where ports are usually defined as communication objects whose methods are invoked within task I/O drivers in a conventional call-return manner, see e.g. [5]. Consequently, the communication pattern is „hardwired‟ in the code of I/O drivers and cannot be reconfigured without reprogramming. The presented model of computation bears certain similarities with the models used in synchronous languages [20], and in particular: atomic execution of input and output actions; clocked operation similar to the execution pattern used in LUSTRE and SIGNAL; compositional data flow models inspired by the Control Engineering domain. Denver, CO, USA, October 6, 2009 54 MoDELS'09 ACES-MB Workshop Proceedings At the same time, there are substantial differences that have to be highlighted in order clearly differentiate the two models: ─ Synthetic, component-based approach using prefabricated executable components vs. a conventional language-based approach used in synchronous languages ─ True actor-level concurrency vs. conceptual concurrency, which is „compiled away‟ during program compilation ─ Constant non-zero reaction time vs. instantaneous (zero-time) reaction assumed by perfectly synchronous systems. The last feature facilitates the engineering of distributed systems and eliminates problems related to fixpoints, instantaneous loops, etc., which have been major issues with synchronous systems. Furthermore, the synchronous model does not address the problem of task and transaction jitter because of the very nature of the synchrony hypothesis, whereas it is practically eliminated with the COMDES model of distributed computation. 5 Conclusion The paper presents the formal specification of COMDES-II - a domain-specific framework for distributed embedded control systems, which combines open architecture and predictable behaviour under hard real-time constraints. The framework employs a hierarchical system model combining the concepts of both actor and function block: an embedded system is composed from autonomous system agents (actors), which are configured from prefabricated executable components – function blocks. Actors interact by exchanging signals, i.e. labeled messages with state message semantics, rather than using I/O ports or operational interfaces. This feature facilitates system reconfiguration and provides for transparent communication between actors, resulting in flexible and truly open distributed systems. Signal-based communication is also used for internal interactions involving constituent function blocks. That is why system configuration is specified by data flow models at all levels of specification. Consequently, actor behaviour is represented as a composition of component functions, and system behaviour – as a composition of actor functions. A synchronous model of computation is applied at the component level. A clocked synchronous model of execution is applied at the actor and system levels, i.e. Distributed Timed Multitasking. The presented software architecture has important implications for software safety and predictability, as well as the entire software development process. In this case, applications are configured from prefabricated and validated (trusted) components, following strict composition rules that are derived from the syntax and static semantics of the framework. The behaviour of software components and applications is rigorously specified via a hierarchy of formal models that constitute the behavioural semantics of the framework. On the other hand, the use of timed multitasking makes it possible to engineer highly predictable systems operating in a flexible, dynamic scheduling environment. This has been demonstrated in a number of experiments used to validate the framework, e.g. distributed computer control systems involving physical and computer models of plants, such as electric DC motor, production cell, steam-boiler, turntable Denver, CO, USA, October 6, 2009 55 MoDELS'09 ACES-MB Workshop Proceedings machine, etc. It has also been applied in an industrial case study - a medical ventilator control system [17]. In all cases, the use of the framework helped reduce development time and increase software quality. This was quite obvious with some of the systems mentioned above, e.g. the production cell control system, which was developed in a relatively short time and became operational without extensive testing and debugging. However, in order to guarantee that an application is correct by construction, it has to be proven correct with respect to the required functional and timing behaviour. That is only possible if a precise and unambiguous system model is developed, whose particular features would desirably facilitate the process of analysis. In COMDES-II that is accomplished through formal design models emphasizing the principle of separation of concerns, i.e. separate treatment of computation and communication, functional and timing behaviour, reactive and transformational behaviour, etc. Thus, different aspects of system behaviour can be verified in separation using appropriate techniques and tools. Functional behaviour can be analyzed using tools such as Simulink (with continuous systems) and Uppaal (with discontinuous systems), following semantics-preserving transformation of system design models into the corresponding analysis models, whereas timing behaviour can be verified through numerical response-time analysis. In particular, Simulink can be used to analyse system behaviour via simulation. That is facilitated by the similarity between COMDES-II design models and Simulink analysis models representing the controller part of the system, both of which are discrete-time data flow models. Consequently, it is possible to export a COMDES-II design model to the Simulink environment, by wrapping COMDES-II components into S-functions and wiring them together, following the interconnection pattern of the original design model. This analysis method has been successfully experimented with the medical ventilator case study, whereby the COMDES-II design of the control system has been exported to Simulink and subsequently validated via numerical simulation. The envisioned development process will make it possible to engineer embedded applications that are correct by construction. This will hopefully eliminate design errors, which are difficult and costly to repair. On the other hand, implementation errors will be eliminated through an automated configuration process supported by an integrated toolchain [16], which is based on meta-models that have been derived from the formal design models presented in this paper. Ultimately, the elimination of both design and implementation errors will considerably enhance software safety, which is of paramount importance for the overall safety of embedded applications. 6 References 1. B. Bouyssounouse and J. Sifakis (Eds.), “Embedded Systems Design. The ARTIST Roadmap for Research and Development”, LNCS 3436 (2005) 2. T.A. Henzinger and J. Sifakis, “The Embedded Systems Design Challenge”, Proc. of the 14th International Symposium on Formal Methods FM 2006, LNCS 4085 (2006), pp. 1-15 3. P. Caspi, “Some Issues In Model-Based Development for Embedded Control Systems”, Invited Lecture, DIPES‟2006, Braga, Portugal, Oct. 2006 Denver, CO, USA, October 6, 2009 56 MoDELS'09 ACES-MB Workshop Proceedings 4. D.B. Stewart, R.A. Volpe and P.K. Khosla, “Design of Dynamically Reconfigurable Real- Time Software Using Port-Based Objects”, IEEE Transactions on Software Engineering, vol. 23, No 12, 1997, pp. 759-776 5. J. Liu and E.A. Lee, “Timed Multitasking for Real-Time Embedded Software”, IEEE Control Systems Magazine: Advances in Software Enabled Control, Feb. 2003, pp. 65-75 6. A. Ghosal, T.A. Henzinger, C.M. Kirsch and M.A. Sanvido, “Event-Driven Programming with Logical Execution Times”, Proc. of HSCC 2004, LNCS 2993 (2004), pp. 357-371 7. D. Isovic and C. Norström, “Components in Real-Time Systems”, Proc. of the 8th International Conference on Real-Time Computing Systems and Applications RTCSA‟2002, Tokyo, Japan, March 2002 8. H. Hansson, M. Åkerholm, I. Crnkovic and M. Törngren, “SaveCCM – A Component Model for Safety-Critical Real-Time Systems”, Proc. of the 30th EUROMICRO Conference on Software Engineering and Advanced Applications SEAA 2004, pp. 627-635 9. A.L. Sangiovanni-Vincentelli and G. Martin, “Platform-Based Design and Software Design Methodology for Embedded Systems”, IEEE Design and Test of Computers, vol. 18 (2001), pp. 23-33 10. K.H. John and M. Tiegelkamp, IEC 61131-3: Programming Industrial Automation Systems, Springer, 2001 11. R. Lewis, Modeling Control Systems Using IEC 61499, Institution of Electrical Engineers (2001) 12. C. Angelov, K. Sierszecki, N. Marian and J. Ma, “A Formal Component Framework for Distributed Embedded Systems”, in I. Gorton et al. (Eds.): Proc. of CBSE 2006, LNCS 4063 (2006), pp. 206-221 13. C. Angelov, X. Ke and K. Sierszecki, “A Component-Based Framework for Distributed Control Systems”, Proc. of the 32nd EUROMICRO Conference on Software Engineering and Advanced Applications SEAA 2006, Cavtat, Dubrovnik, Croatia, Aug.-Sept. 2006, pp. 20-27 14. K. Sierszecki, C. Angelov and X. Ke, “A Run-Time Environment Supporting Real-Time Execution of Embedded Control Applications”, Proc. of the 14th International IEEE Conference on Embedded and Real-Time Computing Systems and Applications RTCSA 2008, Kaohsiung, Taiwan, Aug. 2008 15. C. Angelov, X. Ke, Y. Guo and K. Sierszecki, “Reconfigurable State Machine Components for Embedded Applications”, Proc. of the 34th EUROMICRO Conference on Software Engineering and Advanced Applications SEAA 2008, Parma, Italy, Sept. 2008, pp. 51-58 16. Y. Guo, K. Sierszecki and C. Angelov, “COMDES Development Toolset”, Proc. of the 5th International Workshop on Formal Aspects of Component Software FACS 2008, Malaga, Spain, Sept. 2008, pp. 233-238 17. F. Zhou, W. Guan, K. Sierszecki and C. Angelov, “Component-Based Design of Software for Embedded Control Systems: the Medical Ventilator Case Study”, Proc. of the International Conference on Embedded Software and Systems ICESS 2009, Hanchzhou, China, June 2009 18. W. Henderson, D. Kendall and A. Robson, “Improving the Accuracy of Scheduling Analysis Applied to Distributed Systems”, Real-Time Systems, vol. 20, No 1 (2001), pp. 5- 25 19. A. Jantsch, Modeling Embedded Systems and SoCs - Concurrency and Time in Models of Computation, Morgan Kaufmann, 2003 20. A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic and R. de Simone, “The Synchronous Languages 12 Years Later”, Proc. of the IEEE, vol. 91, No 1, Jan. 2003, pp. 64-83 Denver, CO, USA, October 6, 2009 57