Model-Based Design for Embedded Systems- P19

Chia sẻ: Cong Thanh | Ngày: | Loại File: PDF | Số trang:30

Thêm vào BST

Báo xấu

52
lượt xem 4
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Model-Based Design for Embedded Systems- P19:The unparalleled flexibility of computation has been a key driver and feature bonanza in the development of a wide range of products across a broad and diverse spectrum of applications such as in the automotive aerospace, health care, consumer electronics, etc.The unparalleled flexibility of computation has been a key driver and feature bonanza in the development of a wide range of products across a broad and diverse spectrum of applications such as in the automotive aerospace, health care, consumer electronics, etc....

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Model-Based Design for Embedded Systems- P19

516 Model-Based Design for Embedded Systems The resulting mathematical model is the basis for a precise behavioral semantics for the HRC metamodel and provides a precise semantic for com- ponent composition, an often neglected issue in the design of frameworks for component-based design. Acknowledgment This research has been developed in the framework of the European IP- SPEEDS project number 033471. References 1. R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183–235, 1994. 2. J.-P. Aubin and A. Cellina. Differential Inclusions, Set-Valued Maps and Viability Theory, Grundl. der Math. Wiss., vol. 264, Springer, Berlin/ Heidelberg, 1984. 3. R.-J. Back and J. von Wright. Refinement Calculus: A systematic Introduc- tion. Graduate Texts in Computer Science. Springer-Verlag, New York 1998. 4. R.-J. Back and J. von Wright. Contracts, games, and refinement. Informa- tion and Computation, 156:25–45, 2000. 5. A. Benveniste, B. Caillaud, A. Ferrari, L. Mangeruca, R. Passerone, and C. Sofronis. Multiple viewpoint contract-based specification and design. In Proceedings of the Software Technology Concertation on Formal Methods for Components and Objects (FMCO07), Revised Lectures, Lecture Notes in Computer Science, Amsterdam, the Netherlands, October 24–26, 2007. 6. A. Benveniste, B. Caillaud, and R. Passerone. A generic model of contracts for embedded systems. Rapport de recherche 6214, Institut National de Recherche en Informatique et en Automatique, June 2007. 7. H. Butz. The Airbus approach to open Integrated Modular Avionics (IMA): Technology, functions, industrial processes and future develop- ment road map. In International Workshop on Aircraft System Technologies, Hamburg, Germany, March 2007. 8. A. Chakrabarti, L. de Alfaro, T. A. Henzinger, and M. Stoelinga. Resource interfaces. In Proceedings of the Third Annual Conference on Embedded
Multi-Viewpoint State Machines 517 Software (EMSOFT03), Lecture Notes in Computer Science, Philadelphia, PA, 2855:117–133, 2003. Springer, Berlin/Heidelberg. 9. W. Damm. Controlling speculative design processes using rich compo- nent models. In Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), St. Malo, France, pp. 118–119, June 6–9, 2005. 10. W. Damm. Embedded system development for automotive applica- tions: Trends and challenges. In Proceedings of the Sixth ACM & IEEE International Conference on Embedded Software (EMSOFT06), Seoul, Korea, October 22–25, 2006. 11. L. de Alfaro and T. A. Henzinger. Interface automata. In Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering, Vienna, Austria, pp. 109–120, 2001, ACM Press, New York. 12. E.W. Dijkstra. Guarded commands, nondeterminacy and formal deriva- tion of programs. Communications of the ACM, 18(8):453–457, August 1975. 13. D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed- Independent Circuits. ACM distinguished dissertations. MIT Press, Cambridge, MA, 1989. 14. T. A. Henzinger. The theory of hybrid automata. In LICS, New Brunswick, NJ, p. 278–292, 1996, IEEE Computer Society Press. 15. T. A. Henzinger, R. Jhala, and R. Majumdar. Permissive interfaces. In Pro- ceedings of the 13th Annual Symposium on Foundations of Software Engineer- ing (FSE05), Lisbon, Portugal, pp. 31–40, 2005, ACM Press, New York. 16. Lamport, L. Win and sin: Predicate transformers for concurrency. ACM Transactions on Programming Languages and Systems, 12(3):396–428, July 1990. 17. B. Meyer. Applying “design by contract.” IEEE Computer, 25(10):40–51, October 1992. 18. R. Negulescu. Process spaces. In CONCUR, Lecture Notes in Com- puter Science, University Park, PA, 1877, 2000. Springer-Verlag, Berlin/ Heidelberg. 19. A. Sangiovanni-Vincentelli. Reasoning about the trends and challenges of system level design. Proceedings of the IEEE, 95(3):467–506, 2007.
16 Generic Methodology for the Design of Continuous/Discrete Co-Simulation Tools Luiza Gheorghe, Gabriela Nicolescu, and Hanifa Boucheneb CONTENTS 16.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 520 16.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 521 16.3 Execution Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 523 16.3.1 Global Execution Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 523 16.3.2 Discrete Execution Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 524 16.3.3 Continuous Execution Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 525 16.4 Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 526 16.4.1 Definition of the Operational Semantics for the Synchronization in Continuous/Discrete Global Execution Models . . . . . . . . . . . . . . . . . . . 528 16.4.2 Distribution of the Synchronization Functionality to the Simulation Interfaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 528 16.4.3 Formalization and Verification of the Simulation Interfaces Behavior . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 528 16.4.4 Definition of the Internal Architecture of the Simulation Interfaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 530 16.4.5 Analysis of the Simulation Tools for the Integration in the Co-Simulation Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 530 16.4.6 Implementation of the Library Elements Specific to Different Simulation Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 531 16.5 Continuous/Discrete Synchronization Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 531 16.6 Application of the Methodology . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 533 16.6.1 Discrete Event System Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 533 16.6.2 Timed Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 535 16.6.3 Definition of the Operational Semantics for the Synchronization in C/D Global Execution Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 536 16.6.4 Distribution of the Synchronization Functionality to the Simulation Interfaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 538 16.6.5 Formalization and Verification of the Simulation Interfaces Behavior . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 539 16.6.6 Definition of the Internal Architecture of the Simulation Interfaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 546 16.6.7 Analysis of the Simulation Tools for the Integration in the Co-Simulation Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 549 16.6.8 Implementation of the Library Elements Specific to Different Simulation Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 550 16.7 Formalization and Verification of the Interfaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 550 16.7.1 Discrete Simulator Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 550 519
520 Model-Based Design for Embedded Systems 16.7.2 Continuous Simulator Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 552 16.8 Implementation Stage: CODIS a C/D Co-Simulation Framework . . . . . . . . . . 552 16.9 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 553 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 554 16.1 Introduction The past decade witnessed the shrinking of the chips’ size simultaneously with the expansion of a number of components, heterogeneous architec- tures, and systems specific to different application domains, for example, electronic, mechanics, optics, and radio frequency (RF) integrated on the same chip [16]. These heterogeneous systems enable cost-efficient solutions, an advantageous time-to-market, and high productivity. However, one will notice the increase of the variability of design related parameters. Given their application in various domains such as defense, medical, communication, and automotive, the continuous/discrete (C/D) systems emerge as impor- tant heterogeneous systems. This chapter focuses on these systems, their modeling and simulation. Because of the complexity of these systems, their global design specifi- cation and validation are extremely challenging. The heterogeneity of these systems makes the elaboration of an executable model for the overall simula- tion more difficult. Such a model is very complex; it includes the execution of different components, the interpretation of interconnects, as well as the adap- tation of the components. Their design requires tools with different models of computation and paradigms. The most important concepts manipulated by the discrete and the continuous components are • In discrete models, time represents a global notion for the overall sys- tem and advances discretely when passing by time stamps of events, while in continuous models, the time is a global variable involved in data computation and it advances by integration steps that may be variable. • In discrete models, processes are sensitive to events while in continuous models processes are executed at each integration step [12]. • Each model has to be able to detect, locate in time, and react to events sent by the other model. The International Technology Roadmap for Semiconductors (ITRS) empha- sizes that “a more structured approach to verification demands an effort towards the formalization of a design specification” and that “in the long term, formal techniques will be needed to verify the issues at the boundary of analog and digital, treating them as hybrid systems” [16]. Generally, in the design of embedded systems, the technique favored for the systems validation is co-simulation. Co-simulation allows for the joint
Generic Methodology for the Design 521 simulation of heterogeneous components with different execution models. One of the advantages of this technique is the reusability of the models already developed in a well-known language and using already existing powerful tools (i.e., Simulink R [24] for the continuous domain and VHDL [33], Verilog [31], or SystemC [30] for the discrete domain). Thus, the devel- opment time, the time-to-market, and the cost are reduced. Moreover, this technique allows the designer to use the best tool for each domain and to provide capabilities to validate the overall model. This methodology requires the elaboration of a global simulation model. The global validation of continuous/discrete systems requires co- simulation interfaces providing synchronization models for the accommo- dation of the heterogeneous. The interfaces play also an important role in the accuracy and the performance of the global simulation. This implies a com- plex behavior for the simulation interfaces, their design being time consum- ing and an important source of error. Therefore, their automatic generation is very desirable. An efficient tool for the automatic generation of the simu- lation interfaces must rely on the formal representation of the co-simulation interfaces [29]. This chapter presents a generic methodology, independent of simula- tion language, for the design of continuous/discrete co-simulation tools. This chapter is organized in nine sections. Section 16.2 gives several previ- ous approaches to the modeling of continuous/discrete systems. The exe- cution models for the continuous and the discrete domains are presented in Section 16.3. Section 16.4 details the methodology while Section 16.5 pro- poses a continuous/discrete synchronization model. Section 16.6 exemplifies the application of the methodology described in Section 16.4. Section 16.7 presents the formalization and the verification of the simulation interfaces. An example of a tool implemented with respect to the presented methodol- ogy is shown in Section 16.8. Finally, Section 16.9 gives our conclusions. 16.2 Related Work The existing work on the validation of continuous/discrete heterogeneous systems can be classified into a few categories. They mostly include two approaches: simulation-based approach and formal representation-based approach. The simulation-based approaches can be divided into two groups that use different techniques to obtain the global execution model: 1. The extension of existing tools and languages. Most of the tools cre- ated using this approach started from classical hardware description languages (HDLs) and new concepts specific to other domains such as analog mixed signal (AMS) or synchronous data flow (SDF) ker- nel were added (VHDL-AMS) [15], Verilog-AMS [10], SystemC–AMS
522 Model-Based Design for Embedded Systems [32] or SystemC [27] extended with SDF kernel. These extensions are usually designed from scratch and by consequence their libraries are not as strong as the well established tools for this field (i.e., Simulink). 2. The definition of new models and tools. The systems are designed by assembling different components [23,28]. HyVisual [21] is a systems modeler based on Ptolemy [28] that supports the construction of hier- archal systems for continuous-time dynamical systems (see Chapter 15 and [21]). However, the different subsystems and components need to be developed in the same environment in order to be compatible and therefore they do not solve the problem of IP reuse in system design. Moreover, Ptolemy is based on formal representation, but the formal verification of the simulation models is not considered. In the formal representation-based approaches, the integration is addre- ssed as a composition of models of computation. These approaches propose a single main formalism to represent different models and the main concern is building interfaces between different models of computation (MoC). These approaches bring a deep conceptual understanding of each MoC. In other work [22], a framework of tagged signal models is proposed for comparison of various MoCs. The framework was used to compare certain features of various MoCs such as dataflow, sequential processes, concurrent, sequential processes with rendezvous, Petri nets, and discrete-event systems. The role of computation in abstracting functionalities of complex heterogeneous sys- tems was presented in [17]. In [18] the author proposes the formalization of the heterogeneous systems by separating the communication and the com- putation aspects; however the interfaces between domains were not taken into consideration. In [34], the authors introduce an abstract simulation mechanism that enables event-based, distributed simulation (discrete event system specifications—DEVS), where time advances using a continuous time base. DEVS is a formal approach to build the models, using a hierarchical and modular approach and more recently it integrates object-oriented program- ming techniques. Based on this formalism, [8] has proposed a tool for the modeling and simulation of hybrid systems using Modelica and DEVS. The models are “created using Modelica standard notation and a translator con- verts them into DEVS models” [8]. In [20] the authors propose a heteroge- neous simulation framework using DEVS BUS. NonDEVS-compliant models are converted through a conversion protocol into DEVS-compliant models. CD++ is a general toolkit written in C++ that allows the definition of DEVS and Cell-DEVS models. DEVS-coupled models and Cell-DEVS models can be defined using a high-level specification language [35]. PythonDEVS is a tool for constructing DEVS models and generating Python code. A model is described by deriving coupled and/or atomic DEVS descriptive classes from this architecture, and arranging them in a hierarchical manner through com- position [4]. DEVSim++ is an environment for object-oriented modeling of discrete event systems [19].
Generic Methodology for the Design 523 16.3 Execution Models This section presents the global execution models of continuous/discrete heterogeneous systems. The execution model can be viewed as the interpre- tation of a computation model. Discrete and continuous systems are charac- terized by different physical properties and modeling paradigms. 16.3.1 Global Execution Model The global execution model of a heterogeneous system is the realization of the system’s functionality. A C/D system and its corresponding global exe- cution model are illustrated in Figure 16.1. There are three types of basic elements that compose the model [26]: • The execution models of the different components constituting the het- erogeneous system (corresponding to Component 1 and Component 2 in Figure 16.1) • The co-simulation bus • The co-simulation interfaces The co-simulation bus is in charge of interpreting the interconnections between the different components of the system. The co-simulation interfaces enable the communication of different components through the simulation bus. They are in charge of the adapta- tion of different simulators to the co-simulation bus in order to guarantee the transmission of information between simulators executing the different Discrete component execution model Discrete Co-simulation component interface Co-simulation bus Co-simulation interface Continuous Co-simulation backplane component Continuous component execution model (a) (b) FIGURE 16.1 Continuous/discrete (a) heterogeneous system and its corresponding (b) execution model.
524 Model-Based Design for Embedded Systems components of the heterogeneous systems. They also have to provide efficient synchronization models for the modules adaptation. The co-simulation backplane is the element of the global execution model that guarantees the synchronization and the communication between the dif- ferent components of the system. It is composed of the above mentioned sim- ulation interfaces and the simulation bus. The implementation and the simulation of an execution model in a given context is called co-simulation instance. Several instances may correspond to the same execution model and these instances may use different simulators and may present different characteristics (e.g., accuracy and performances). 16.3.2 Discrete Execution Model The execution model for a discrete system is a model where changes in the state of the system occur at discrete points in the execution time. The discrete system can be described by the state–space equations [6]: ⎧ ⎨xd (tk+1 ) = f (xd (tk ), u(tk ), tk ) with x(t0 ) = x0 (16.1) ⎩ y(tk ) = g(xd (tk ), u(tk ), tk ) where f and g are transformations xd is the discrete state vector u is the input signal vector y is the output signal vector For the linear discrete systems, Equation 16.1 becomes ⎧ ⎨xd (tk+1 ) = Ad xd (tk ) + Bd u(tk ) (16.2) ⎩ y(tk ) = Cd xd (tk ) + Dd u(tk ) where Ad , Bd , Cd , and Dd are matrices that can be time varying and describe the dynamics of the system [6]. A discrete event system execution concentrates on processing events, each event having assigned a time stamp. Each event computation can mod- ify the state variables, schedule new events or retract existing events. The unprocessed events are stored in a pending events list. The events are pro- cessed in the order of their time stamp. Figure 16.2 shows a possible update event schema. At each simulation cycle, the first event with the smallest time stamp is processed and the processes sensitive to this event are executed [34]. If several processes are sensitive to one or several events (with the same time occurrence) then these processes have to be executed in parallel. Execu- tions often occur on sequential machines that can only execute one instruc- tion at a time (therefore, one process). The consequence is that this execution
Generic Methodology for the Design 525 Start State Event Scheduled time State1 e1 t1 State2 e2 t2 State3 e3 t3 Clock = t1, e1 removed and executed No Is queue Yes re-ordered? e2 t2 e'2 t'2 e3 t3 e'3 t'3 e4 t4 e'4 t'4 Update state Update state variables variables Stop Stop FIGURE 16.2 Event update schema. cannot parallelize the processes. The solution consists in emulating the par- allelism, where the processes are executed as if the parallelism is real and the environment does not change while executing all the processes. Once all events with discrete time stamp equal to the current time have been treated, the simulator advances the time to the nearest scheduled discrete event. 16.3.3 Continuous Execution Model The continuous time system is described by the state–space equations: ⎧• ⎨xc (t) = Ac xc (t) + Bc u(t) (16.3) ⎩ y(t) = Cc xc (t) + Dc u(t) where xc is the state vector u is the input signal vector y is the output signal vector Ac , Bc , Cc , and Dc are constant matrices that describe the dynamic of the system
526 Model-Based Design for Embedded Systems The execution of continuous model, described by differential and algebraic equations, requires solving these equations numerically. A widely used class of algorithms discretizes the continuous time line into an increasing set of discrete time instants, and numerically computes values of state variables at these ordered time instants. The next state of derivative systems cannot be specified directly but the derivative functions are used to specify the rate of change of state variables [34]. The execution of a continuous system raises problems because given a state qk and a vector x for a time tk , the derivative offers information only for dqk /dt but not the system’s behavior over time. For a nonzero interval [tk , tk+1 ] the computation has to be realized without knowing the behavior in the interval (tk , tk+1 ). This problem can be solved using numerical integration methods. Some of the most commonly used methods are • Euler method that consists in signal integration: dq(t) lim q(t + h) − q(t) = . dt h→∞ h For an h small enough (in order to obtain accurate results), the following approximation can be used: dq(t) q(t + h) = q(t) + h ∗ d(t) This solution has low efficiency and does not have stability problems for small enough h and it is very robust [34]. • Causal methods that are a linear combination of states and derivative values at time instants with coefficients chosen to minimize errors from the computed estimate to the real value [34]. This solution has high efficiency but it has stability and robustness problems. • Noncausal methods that use “future” values of states, derivative, and inputs. In order to do that the model is executed past the needed time and the values that are necessary are stored to estimate the present values [34]. 16.4 Methodology This section introduces a methodology for the design of continuous/dis- crete co-simulation tools (as shown in Figure 16.3). To enable the design of co-simulation tools, this methodology presents several steps that are inde- pendent of the simulation tools used for the continuous and discrete
Generic Methodology for the Design 527 Generic stage Definition of the operational semantics for the synchronization Distribution of the synchronization functionality to the interfaces Formalization and verification of the interfaces behavior Definition of the internal architecture of the interfaces and the library elements Simulation Library elements tools analysis implementation Implementation Implementation stage validation FIGURE 16.3 A generic methodology for the design of C/D co-simulation tools. components of the system. During these generic steps, the co-simulation interfaces are defined in a conceptual framework; their functionality and the internal structure of simulation interfaces are expressed using exist- ing formalisms and temporal logic. After the rigorous definition of the required functionality for simulation interfaces, the designer will start the steps related to the implementation. The main steps of the proposed methodology (illustrated in Figure 16.3) can be divided into two stages: 1. A generic stage with the following actions: • Definition of the operational semantics for the synchronization in continuous/discrete global execution models. • Distribution of the synchronization functionality to the simulation interfaces. • Formalization and verification of the simulation interfaces behavior. • Definition of the library elements and the internal architecture of the simulation interfaces. 2. An implementation stage with the following actions: • The analysis of the simulation tools for the integration in the co- simulation framework. • The implementation of the library elements specific to different sim- ulation tools.
528 Model-Based Design for Embedded Systems This section focuses on the generic stage and its steps will be detailed in the next subsections. A possible implementation stage will be detailed further in Section 16.8. 16.4.1 Deﬁnition of the Operational Semantics for the Synchronization in Continuous/Discrete Global Execution Models The first step of the methodology for co-simulation tools design is the defini- tion of the operational semantics for the synchronization in continuous/dis- crete global execution models. An operational semantics gives a detailed description of the system’s behavior in mathematical terms. This model serves as a basis for analysis and verification. The description provides a clear language independent model that can serve as a reference for different implementations. The operational semantics for continuous/discrete systems requires the rigorous representation of the relation between the simulators (communica- tion/synchronization and data exchanged between the continuous and the discrete simulators) as well as their high level and dynamic representations. 16.4.2 Distribution of the Synchronization Functionality to the Simulation Interfaces Based on the operational semantics, we can now define the synchronization functionality between the continuous and the discrete simulators. This func- tionality is insured by the interfaces that are the link between the different execution models and the co-simulation bus (see Figure 16.1). They are each in charge with a part of the synchronization between the two models. To ensure system’s flexibility, the synchronization functionality has to be dis- tributed to the simulation interfaces. Moreover, each computation step has to be thoroughly specified. 16.4.3 Formalization and Veriﬁcation of the Simulation Interfaces Behavior The formalization and verification of the simulation interfaces behavior stage can be roughly divided in three steps: formalization (that can be the formal specification of the heterogeneous system), the validation by model simula- tion, and the formal verification. The two main techniques that can be used for the formal verification of the interfaces are [36]: • Model checking, where the system descriptions are given as automata, the specification formulas are given as temporal logic formulas, and the checking consists of the verification which ensures that all models of a given system description satisfy a given specification formula. It
Generic Methodology for the Design 529 focuses mainly on automatic verification. Completeness and termination guarantee of model checking are some features of this technique, as well as it enables the tool to guarantee the correctness of a given property, or produce a counterexample otherwise. • Theorem proving, where the verification plan is manually designed and the correctness of the steps in the plan is verified using theo- rem provers. Completely automatic decision procedures are impos- sible because the input language (the model and the specification) is of higher order logic and that eliminates the decidability. Moreover, everything has to be translated in higher order logic, and, therefore, the structure of the system may be lost and its representation can become large and difficult to work with. Considering that the system is dynamic, it is necessary to use a formal- ism that allows the expression of dynamic properties (the state of a system changes and by consequence the properties of the state also change). The temporal logic handles formalization where the properties evolve over time and in general uses: • Propositions that describe the states (i.e., elementary formulas and log- ical connectors) • Temporal operators that allow the expression of the properties of the states successions (called executions) The differences between the logics are in terms of temporal operators and objects on which they are interpreted (such as sequences or state trees) [25]. The most commonly used logics are Linear Temporal Logic (LTL), Com- putation Tree Logic (CTL* and CTL, both of them untimed temporal log- ics) and their timed extensions TCTL and Metric Interval Temporal Logic (MITL). • CTL* allows the use of all temporal and branching operators but the property verification is very complex. For this reason, most of the tools actually used allow the verification of fragments of CTL*. • LTL is a fragment of CTL* that excludes the trajectory quantifiers. In this case only the trajectory predicates are considered. LTL does not provide a means for considering the existence of different possible behaviors starting from a given state (sequential) 0. • CTL is also a fragment of CTL* and it is obtained when every occur- rence of a temporal operator is immediately preceded by a branching operator. In the case of CTL we have state trees. • TCTL is a timed temporal logic that is an extension of CTL obtained by subscribing the modalities with time intervals specifying time restric- tions on formulas. For our formal model, the properties that need to be checked are branching properties that are expressed using CTL or TCTL logics.
530 Model-Based Design for Embedded Systems Continuous/discrete global simulation model Continuous Continuous/discrete Discrete model simulation interface model Continuous domain Discrete domain simulation simulation interface-CDI interface-DDI Atomic model Atomic model Atomic model Atomic model CDI CDI CDI CDI Co-simulation Atomic model Atomic model bus Atomic model Atomic model CDI CDI CDI CDI Atomic model CDI Elements from the co-simulation library FIGURE 16.4 Hierarchical representation of the generic architecture of the co-simulation model. 16.4.4 Deﬁnition of the Internal Architecture of the Simulation Interfaces The formalization of the simulation interfaces behavior step is naturally fol- lowed by the definition of their internal architecture. This definition eases the automatic generation of the simulation interfaces. We present in Figure 16.4 the hierarchical representation of the global simulation model used in our approach. At the top hierarchical level, the global model is composed of the contin- uous and discrete models and of the C/D simulation interface required for the global simulation [12]. The second hierarchical level of the global simulation model includes the domain specific simulation interfaces and the co-simulation bus in charge of the data transfer between these interfaces. The bottom hierarchical level includes the elements from the co- simulation library that are the atomic modules of the domain specific sim- ulation interface. These atomic components implement basic functionalities of the synchronization model. 16.4.5 Analysis of the Simulation Tools for the Integration in the Co-Simulation Framework The considerations presented in the previous steps of the methodology show that specific functionalities are required for the co-simulation of continu- ous and discrete modes. Therefore, the integration of a simulation tool in
Generic Methodology for the Design 531 the co-simulation environment requires their analysis. Thus, in the case of continuous simulator integration in the co-simulation tool, this simulator has to provide application programming interfaces (APIs) enabling the following controls: • Detection and location of state events • Setting break points during differential equation solving • Online update of the breakpoints settings • Sending processing results and information for synchronization (i.e., the time step of the state event) to the discrete simulator. This generally implies the possibility to integrate C-code and Inter-Process Commu- nications (IPC). For the integration of a discrete simulator in the co-simulation tool, the sim- ulator has to enable the addition of the following functionalities: • Detection for the end simulation cycle • Insertion or retraction of new events (state events) in the scheduler’s queue. This must be done before the advancement of the simulator time • Sending processing results and information for synchronization to the continuous simulator (i.e., the time stamp of its next discrete event). 16.4.6 Implementation of the Library Elements Speciﬁc to Different Simulation Tools The last step of the methodology for the design of co-simulation tools for continuous/discrete systems is the implementation of the library elements that are specific to different simulation tools. This step depends highly on the simulation tools chosen in the previous step, the analysis of the simulation tools. 16.5 Continuous/Discrete Synchronization Model The methodology focuses mostly on the co-simulation interfaces. One of the most important functions of the interfaces is providing the synchronization that is defined as coordination with respect to time. Thus, for a better under- standing of the methodology it is very important for one to comprehend the synchronization model. The synchronization between the continuous-time domain and the discrete-event domain is realized using a canonical algo- rithm as it was presented in [11]. For a rigorous synchronization the discrete kernel has to detect the events generated by the analog (continuous) solver
532 Model-Based Design for Embedded Systems and the continuous solver must detect the scheduled events from the discrete kernel. The events exchanged between the discrete and the continuous simula- tors are [7]: • Occurred/scheduled events that are timed events scheduled by the dis- crete simulator. • State events that are unpredictable events generated by the continuous simulator. Their time stamp depends on the values of state variables (e.g., a zero-passing or a threshold crossing). For the discrete event processes, time does not advance during the execution. The next execution time is the time of the next event in the event queue. The execution of the analog solver advances the simulation time. Let tk be the synchronization time for the discrete kernel and the analog solver. The ana- log solver advances to the next synchronization time tk+1 , known in advance from the digital kernel. At this point the analog solver suspends while the digital kernel resumes and the events in tk+1 are executed. If a state event occurs in the time interval [tk , tk+1 ], the analog solver suspends to allow the digital kernel to take this event into consideration. This way the analog solver and the digital kernel are synchronized again. Figure 16.5a presents the synchronization model in the C/D co- simulation interface without taking into consideration the state event occur- rence. The state event is taken into consideration in Figure 16.5b. At a given time, the discrete simulator is in the state (xdk ,tk ). At this point, the discrete simulator has executed all the processes sensitive to the event with the time stamp tk and sends the time of the next event tk+1 and the data to the continuous simulator and the context is switched from the discrete to the continuous simulator before advancing the time. Discrete (xdk, tk) 4 (xdk + 1, tk + 1) (xdk , tk) 4 (xdse, tse) (xdk΄, tk΄) simulator t 1 3 5 3 5 1 (Data, tk + 1) (Data) (Data, tk + 2) (Data, tk΄) (Data, tk + 1) Continuous (Data, tse) simulator t (xck , tk) 2 (q, tk + 1) 2 (xck, tk) (se, tse) (xck΄, tk΄) No state event State event (a) (b) Scheduled event Reached event Synchronization State event Simulation step FIGURE 16.5 The synchronization model in the C/D simulation interface without state event (a) or with state event (b).
Generic Methodology for the Design 533 The state of the continuous simulator is (xck ,tk ) and the advance in time of the simulator cannot be further than tk+1 , the time sent by the discrete simu- lator. Consequently, the continuous simulator computes signals by resolv- ing the system’s equations until it reaches with accuracy the time tdk+1 , updates signals with the values calculated at this time its new state being (q, tk+1 ), sends the new data, and the context is switched to the discrete model (arrow 3). The discrete simulator will also advance to the time tk+1 (arrow 4) and the cycle restarts as shown in Figure 16.5a. The continuous model may generate a state event. In this case, it updates signals with the values calcu- lated at this time, tse in Figure 16.5b its new state being, (se, tse ), it indicates its presence by sending the state event’s time stamp (tse ) and the correspond- ing data to the discrete model before switching the simulation context. The discrete model has to be able to detect this event, by advancing the local time to the time stamp, and to execute the processes that are sensitive to it and arrive at the state (xdse , tse ). 16.6 Application of the Methodology This section proposes a possible application of the methodology that was proposed in Section 16.4. First, the basic concepts that are used in our specific methodology are introduced: DEVS and timed automata [1]. 16.6.1 Discrete Event System Speciﬁcations DEVS is a formalism supporting a full range of dynamic system represen- tation, with hierarchical and modular model development. The abstraction separates modeling from simulation and provides atomic models that can be used to build complex models that allow the integration of continuous and discrete-event models [34]. It also provides all the mechanisms for the defini- tion of an operational semantics for the continuous/discrete synchronization model, the high level representation of the global formal model. A DEVS is defined as a structure [34]. DEVS = < X, S, Y, δint , δext , λ, ta > where X = {(pd , vd )|pd ∈ InPorts, vd ∈ Xpd } set of input ports and their values in the discrete event domain, S—set of sequential states Y = {(pd , vd )|pd , ∈ OutPorts, vd ∈ Ypd } set of output ports and their values in the discrete event domain. δint : S→ S the internal transition function δext : QxX→ S the external transition function, where: Q = {(s, e)|s ∈ S, 0 ≤ e ≤ ta(s)} set of total state, e is the time elapsed since the last transition
534 Model-Based Design for Embedded Systems λ : S→Y output function ta : S→R+ set of positive reals with 0 and ∞. 0,∞ The system’s state at any time is s. There are two possible situations: • Case 1—where we assume that no external events occur. In this case the system stays in this state s for the time ta (s). When the elapsed time e equals ta (s) (that is the time allocated for the system to stay in state s), the system outputs the value λ(s). The state s changes to the state s as a result of the transition δint (s). We emphasize here that the output is possible only before the internal transitions. We propose the definition of this type of transition using the following rule of the form Premises : e=ta (s)∧s =δint (s) , where “!” represents the send oper- !λ(s) Conclusions (s,e)− (s ,0) → ator. • Case 2—where there is an external event x before the expiration time, ta (s) (the system is in state (s,e), with e ≤ ta (s)), the system’s state changes to state s as a result of the transition δext (s, e, x). For the definition of this type of transition, we propose the following rule: e≤ta (s)∧s = δext (s,e,x) ?x , where “?” represents the receive operator. (s,e)− (s ,0) → Thus, the internal transition function dictates the system’s new state when no external events occurred since the last transition while the external transition function dictates the system’s new state when an external event occurs—this state is determined by the input x, the current state s and the time period during which the system has been in this state, e. In both cases the system is then in some new state s with some new expiration time ta (s ). We also give here DEVS coupled models as defined by the same formal- ism. For the case where we have ports, the specification includes external interfaces with input and output ports and values and coupling relations: • N = (X,Y,D, {Md |d ∈ D}, EIC,EOC,IC) where: • X = {(p, v)|p ∈ InPorts, v ∈ Xp} set of input ports and values • Y = {(p, v)|p ∈ OutPorts, v ∈ Yp} set of output ports and values • D = set of components names • Md = ( Xd , S, Yd , δint , δext , λ, ta ) is a DEVS with Xd , Yd the set of input/output ports and values • EIC (External Input Coupling) = the coupling between the input in the coupled model and the external environment • EOC (External Output Coupling) = the coupling between the output from the coupled model and the external environment • IC (Internal Coupling) = the coupling between the modules that com- pose the coupled module [12] In our work we used the parallel DEVS coupled formalism. Each module composing the interface performs a different task according to the synchro- nization model specified in Section 16.5.
Generic Methodology for the Design 535 16.6.2 Timed Automata In this section we briefly introduce timed automata. Chapter 14 gives a more detailed presentation of this formalism. A timed automaton [1] is the for- malism for modeling and verification of real time systems. It can be seen as classical finite state automata with clock variables and logical formulas on the clock (temporal constraints) [3]. The constraints on the clock variables are used to restrict the behavior of the automaton. The logical clocks in the system are initialized to zero when the system is started and then increase at the uniform rate counting time with respect to a fixed global time frame. Each clock can be separately reset to zero. The clocks keep track of the time elapsed since the last reset [1]. There are two types of clock constraints: con- straints associated with transitions and constraints associated with locations. A transition can be taken when the clocks’ values satisfy the guard labeled on it. Figure 16.6 illustrates an example of a timed automaton. The constraints associated with locations are called invariants and they specify the amount of time that may be spent in a location. The invariant “true” for a location means there are no constraints for the time spent in the location. The process shown in Figure 16.6 starts at the location p with all its clocks (x and y) initialized to 0. The values of the clocks increase synchronously with time at the location q. At any time, the process can change the location following a transition g;a;r p −→ q if the current values of the clocks satisfy the enabling condition g (guard). A guard is a Boolean combination of integer bounds on clocks and Guard Action Reset Invariant y