A Model for Component Based Development of Embedded Software
The increasing size and complexity of embedded systems poses a serious challenge in design due to diverse, severe and conflicting requirements, and then in verifying their correctness. Some approaches for design and verification have been proposed 2, 3. Component Based Development (CBD) 3 is a change of focus from algorithmic and data structure related issues to the overall architecture of a software system, where the architecture is meant to be a collection of components together with a description of their interconnection topology. A better structure can bring predictable and guaranteed behaviour under hard real-time constraints; scalable and open architecture supporting both design and analysis reuse. Model checking 5 is an important method for improving reliability of software systems. It provides computation of the satisfaction of temporal logics formulae upon transition system being checked and is particularly effective at detecting functional errors (i.e. correct use of resources, correct event ordering and precedence w.r.t. data, coordination towards a scope, desirable dynamic behaviour), which frequently result from component compositions and are notoriously difficult to detect. However, model checking often cannot handle large-scale software systems due to state space (i.e. states × variables)explosion. Model checking and CBD are mutual enhancing. Model checking can potentially enable effective development of more reliable component-based software systems. CBD introduces compositional structures, clean component interfaces, and standard composition rules to the systems being built, which may reduce the state spaces that model checkers have to compute. The Software Engineering Group of the Mads Clausen Institute for Product Innovation (MCI)has developed an integrated approach to design and verification called COMDES (Component-based Design of Software for Embedded Systems), in an attempt to find a solution to the outlined problems. The advantages of the method are the well structuredness and reusability of the design and verification. Under COMDES, a distributed embedded application is specified in terms of interacting subsystems (function units, FUs), such as sensor, controI unit, actuator, operator station, etc. 1. FUs are defined as software integrated circuits encapsulating one or more dynamically scheduled tasks (activities) that are configured from prefabricated lower-level components such as function blocks (FBs) and reconfigurable state machines (SMs). The composition of interacting subsystems is synchronous in the way adopted by the synchronous model and languages 6, i.e. every subsystem that can make a transition upon its inputs in an execution instance, does so. The reconfigurable feature of the SM resides in using standard high-level solutions based on advanced techniques, i.e. binary decision diagrams (BDD). These have been instrumental in developing design patterns for reusable and reconfigurable components such as the state-logic controller (SLC) and hybrid SLC (HSLC), which can be used to implement SMs of arbitrary complexity, including hierarchical and concurrent SMs. Analysis of system behaviour is a highly complex problem,which has been extensively studied over the years but no comprehensive solution has emerged as yet 5. A practical approach to systems analysis has to take into account the specific features of the system model used. That is the case with CBD, which is inherently based on the adoption of such a model (framework) that has to explicitly specify all aspects of system structure and behaviour (e.g. COMDES). Compositional specification of component-based systems is naturally combined with compositional verification, which might also be denoted as modular reasoning 4. The strategy is to verify the subsystems and components separately, and then by using a suitable inference rule, make conclusions about the correctness of the system as a whole.Compositional verification 4 in our case exploits the hierarchical structure of COMDES to divide a verification task into subtasks. Given a requirement R that a system must satisfy, the compositional rule allow for a systematic bottom-up or top-down modular verification method. The COMDES model combines in a natural way reactive (event-related) and transformational (datarelated) aspects of system behaviour. At the same time, these two aspects are clearly separated i.e. the model specifies which reactions have to be generated in response to certain events, and how these reactions are to be generated within the corresponding system states. That is why it is possible to treat them in separation: event-driven behaviour can be checked with respect to events and reactions using an appropriate technique, e.g. model checking. Data transformations might be verified via symbolic data manipulations and assertion compositional proofs integrated in model checking through guaranteed constructs 4, 5. Each FB or composite FB have an associated set of guaranteed assertions corresponding to the continuous state trajectory evolving in Rn. Predicates include threshold post condition boolean events and abstracted signals. Correctness properties can be expressed in CTL formulas and the whole model can be translated native (due to symbolic next state mappings of SLCs, HSLCs) in SMV 5, using a similar approach as in 7.Combination of formal verification and testing is also effective at detecting functional errors. Timing correctness is addressed by applying schedulability analysis with respect to real-time deadlines imposed on the execution of FU activities (tasks) and distributed transactions. However, real-time scheduling theory assumes a periodic execution framework, i.e. all activities have to behave as periodic tasks. This poses no problems with activities that are inherently periodic but aperiodic activities have to be modeled as pseudoperiodic (sporadic) tasks. Alternatively, event-driven SMs might be transformed into equivalent time-driven SMs having periodic execution patterns 6. The ultimate goal of our effort is to create an integrated software development environment consisting of software configuration and analysis tools that will make it possible to configure and verify embedded applications using formal models and standardized prefabricated proved components, much in the same way as that is done in mature areas of engineering such as Mechanical Engineering and Electronics.
Nicolae Marian
Mads Clausen Institute for Product Innovation, University of Southern Denmark,Grundtvigs Alle 150, 6400 Soenderborg, Denmark
国际会议
首届嵌入式软件与系统国际会议(Proceedings of the First International Conference on Embedded Software and System)
杭州
英文
575-576
2004-12-09（万方平台首次上网日期，不代表论文的发表时间）