Model-driven design and
ASM-based validation of
Embedded Systems
Angelo Gargantini
Dipartimento di Ingegneria Informatica e Modelli Matematici, Università di Bergamo, Italy -
Elvinia Riccobene
Dipartimento di Tecnologie dell’Informazione,Università di Milano, Italy
Patrizia Scandurra
Dipartimento di Tecnologie dell’Informazione, Università di Milano, Italy
Key Terms & Definitions
Model-driven engineering, Embedded System Design, System on Chip Design, Abstract State Machines, UML profile, SystemC, Behavioral modeling, System Validation.
Abstract
In the embedded system and System-on-Chip (SoC) design area, the increasing technological complexity coupled with requests for more performance and shorter time to market have caused a high interest for new methods, languages and tools capable of operating at higher levels of abstraction than the conventional system level. This chapter presents a model-driven and tool-assisted development process of SoCs, which is based on high-level UML design of system components, guarantees SystemC code generation from graphical models, and allows validation of system behaviors on formal models automatically derived from UML models. An environment for system design and analysis is also presented, which is based on a UML profile for SystemC and the Abstract State Machine formal method.
Introduction
In the Embedded System (ES) and System-on-Chip (SoC) design area, conventional system level design flows usually start by writing the system specification and developing a functional executable model. The system is refined through a set of abstraction levels, toward a final implementation in hardware and software. Nowadays it is an emerging practice to develop the functional model and refine it with the C/C++/SystemC languages[Gröetker et al., 2002]. The hardware part of the system goes down to the Register Transfer Level (RTL) for the synthesis flow, while the software part can be either simulated at high (functional or transactional) level or compiled for an Instruction Set Simulator (ISS).
Recently, the increasing technological complexity coupled with requests for more performance and shorter time to market have caused a high interest for new methods, languages and tools capable of operating at higher levels of abstraction in the design process. Such an improvement has been achieved by exploiting visual software modelinglanguages like Unified Modeling Language (UML) [UML, 2005] to describe system specifications and generate from them executable models in C/C++/SystemC.
In the embedded system domain, the UML has been used mainly for documentation purposes. There are, indeed, some criticisms that are widely shared towards the use of the UML as modeling language. The UML includes a rich set of modeling elements that can be used for a wide range of applications, whereas modeling specific applications, as embedded systems and SoCs, would be easier using a more specialized (domain-specific) notation representing the basic elements and patterns of the target domain. Furthermore, the UML offers the possibility of designing the same system from different views (by different UML diagrams). Even if such a feature can be used to capture related aspects of a design from different prospective, it may result in inconsistencies between diagrams, when the use of UML is not coupled with a rigorous design discipline [Chen et al, 2003
]. Therefore, the use of the UML for the specific application domain of embedded system and SoC design requires:
- a domain specific language, called profile, built on the basic UML infrastructure and including domain-specific building blocks (defined using stereotypes) to model common design elements and patterns,
- a methodology defining how and when the profile notation should be used.
According to these requirements, in [Riccobene et al., 2005a, Riccobene et al., 2005b, Riccobene et al., 2007a] a UML2 profile for SystemC is presented, which lifts the SystemC language to the UML modeling level. It represents a set of structural and behavioral constructs for designing at system-level with automatic encoding in SystemC. With this approach, the standard UML language is applied as high-level system modeling language and operates in synergy with a lower-level system language. To foster the methodology in a systematic and seamless way, in [Riccobene et al., 2007b] a SoC design process, called UPSoC (Unified Process for SoC), is presented as extension of the conventional Unified Process [Arlow & Neustadt, 2002]for the SoC refinement flow. The UPSoC process has been developed following the principles of the Object Management Group (OMG) Model-driven Architecture (MDA) [Mellor et al., 2003] -- a framework for Model-driven Engineering(MDE) [Bezivin, 2005], according towhich a system development process should relyon modeling, model transformations and automatedmapping of models to implementations. Indeed, the UPSoC is based on model-to-model and model-to-code model transformations from abstract models towards refined (but still abstract) models and/or SystemC code models.
Even if modeling methods based on the UML and UML profiles have receiving increasing interest in the embedded system and SoC contexts as they allow modeling at a higher level of abstraction than that of system-level languages, UML-based design methods still suffer the lack of effective formal analysis (validation & verification) techniques. Formal methods and analysis tools have been most often applied to low level hardware design. But, these techniques are not applicable to system descriptions given in terms of programs of system-level languages (like SystemC, SpecC, etc.), since such languages are closer to concurrent software than to traditional hardware description [Vardi, 2007], and the focus in the literature so far has been mainly on traditional code-based simulation techniques. Moreover, classical analysis techniques are not directly applicable to UML-based design methods that lack of a strong mathematical foundation necessary for formal model analysis.
We tackle the problem of formally analyzing high-level UMLSoC descriptions by joining the SystemC UML modeling language with a formal method, capable of eliminating ambiguities in the UML semantics, and using analysistechniques applicable to formal models. Therefore, we have complementedourUPSoC design process with a formal analysisprocess allowing system components to be functionally validated and verified early at high levels of abstraction, and even in a semi-transparent way (i.e. no strong skills and expertise on formal methods are required to the user) by the use of the Abstract State Machine (ASM) formal method [Börger & Stärk, 2003] and its related tools [Asmeta, 2007].
In this chapter, we present a model-driven methodology for the SoC design, which involves the SystemC UML profile as major system modeling notationand the Abstract State Machinesas formal support for validation of system behavior. The modeling activity can be performed at different levels of abstraction, from a highfunctionallevel down to the Register TransferLevel (RTL). Model-to-code transformations allow automatic mapping of UML models to SystemC code, while model-to-model transformations provide automatic mapping of SystemC UML graphical model to formal models suitable for application of model analyses standard techniques.
A supporting environment for both processes of SoC design and validation is also presented. The modeling kit of this environmentassists the designer along the modeling activityand provides SystemC code generation/back-annotation from/to UML modes. The validation process is supported by an analysis kit built upon the ASMETA toolset – a set of tools around ASMs --, which operates on the formal specification of the system.
As case study, the Counter system taken from the standard SystemC distribution will be considered to illustrate how to design and validate a SoC by our approach. The design model is developed using the SystemC UML profile. We then show how the UML model of the underlying system is automatically mapped into a corresponding ASM model, and how to validate the system functionality by techniques based on simulation and scenarios construction.
The remainder of this chapter is organized as follows. Sect. Background quotes some related work and provides an overview of the SystemC UML profile explaining the rationality behind the development of a UML profile forthe SoC design. It also briefly summarizes the application of formal methods to specify and analyze embedded systems, and presents and justifies the choice of the ASMsas formal support for our design methodology. Sect. Model-driven SoC design and analysis flow describes the overall SoC design and analyses flow, at the light of the MDA principles. It also comments on the advantages of a model-driven methodology with respect to a code design for the development of SoCs. Sect. SoC modeling & Validation environment describes the architecture and the tool components of the supporting design and validation environment. Sect. The Counter case study presents the application of our design methodology to the case study. Sect. Industrial application discusses some industrial case studies. Sect. Future Trends sketches some future directions. Finally, Sect. Conclusion provides some concluding remarks.
Background
This section provides an overview ofexisting work concerning model-driven approaches for embedded system and SoC modeling using UML and UML profiles, and on the formal analyses of UML design models. It also introduces the reader to the main notations used in our approach, namely the UML profile of the SystemC language and the Abstract State Machines. It also justifies the choice of the formal method we use for analyses purposes, in relation to the models of computation most commonly used in the area of embedded system and SoC modeling.
Related work
The possibility to use UML 1.x for system design [Martin, 1999] started since 1999, but the general opinion at that time was that UML was not mature enough as a system design language. Nevertheless significant industrial experiences using UML in a system design process soon started leading to the first results in design methodology, such as the one in [Moore et al., 2002] that was applied to an internal project for the development of a OFDM Wireless LAN chipset. In that project, SystemC was used to provide executable models.
More integrated design methodologies were later developed. The authors of [Zhu et al., 2004] propose a methodology using UML for the specification and validation of SoC design. They define a flow, parallel to the implementation flow, which is focused on high-level specs capture and validation. In [Lavagno et al., 2003], a UML profile for a platform-based approach to embedded software development is presented. It includes stereotypes to represent platform services and resources that can be assembled together. The authors also present a design methodology supported by a design environment, called Metropolis, where a set of UML diagrams (use cases, classes, state machines, activity and sequence diagrams) can be used to capture the functionality and then refine it by adding models of computation. Another approach to the unification of UML and SoC design is the HASoC (Hardware and Software Objects on Chip) [Edwards & Green, 2003] methodology. It is based on the UML-RT profile [Selic, 2003] and on the RUP process [Kruchten, 1999]. The design process starts with an uncommitted model, then a committed model is derived by partitioning the system into software and hardware, which is finally mapped onto a system platform. From these models a SystemC skeleton code can be also generated, but to provide a finer degree of behavioral validation, detailed C++ code must be added by hand to the skeleton code. All the works mentioned above could greatly benefit from the use of UML2 [UML, 2005].
In [do Nascimento et al., 2007], the authors present a model-driven framework, called ModES (Model-driven Design of ES), made of metamodels definition and APIs to integrate, by model transformations, several model-based design tools. However, this framework is more related to the design space exploration at a high abstraction level than to model refinement, model validation, andautomatic code generation from models, which are, instead, our main concerns.
SysML [SysML, 2007] is an extension of the UML2 for a domain-neutral representation of system engineering applications. It can be involved at the beginning of the design process, in place of the UML, for the requirements, analysis, and functional design workflows. So it is in agreement with the SystemC UML profile, which can be thought (and effectively made) as customization of SysML rather than UML. Unluckily, when we started the SysML specification was not yet finalized and there were no tools yetsupporting it. Similar considerations apply also to the recent MARTE (Modeling and Analysis of Real-Time Embedded Systems) profile initiative [Rioux et al., 2005;MARTE, 2008].
The standardization proposal [USoC, 2005] by Fujitsu, in collaboration with IBM and NEC, has evident similarities with the SystemC UML profile, like the choice of SystemC as a target implementation language. However, their profile does not provide building blocks for behaviormodeling, neither any time model.
Some other proposals already exist about extensions of UML towards C/C++/SystemC. All have in common the use of UML stereotypes for SystemC constructs, but do not rely on a UML profile definition. In this sense, it is appreciable the work in [Bruschi & Sciuto, 2002] attempting to define a UML profile for SystemC; but, as all the other proposals, it is based on the previous version of UML, UML 1.4. Moreover, in all the proposals we have seen, no code generation, except in [Nguyen et al., 2005], from behavioral diagrams is considered.
Concerning the analysis (i.e. the validation and verification) of UML-based embedded system descriptions, in [Patel & Shukla, 2007] the authors present a model-driven development and validation process which begins by creating (from a natural language specification of the system requirements) a functional abstract model and (still manually) a SystemC implementation model. The abstract model is described using the Abstract State Machine Language (AsmL) – another implementation language for ASMs. Our methodology, instead, benefits from the use of the UML as design entry-level and of model translators that provide automation and ensure consistency among descriptions in different notations (such those in SystemC and ASMs). In [Patel & Shukla, 2007], a designer can visually explore the actions of interest in the ASM model using the Spec Explorer tool and generate tests. These tests are used to drive the SystemC implementation from the ASM model to check whether the implementation model conforms to the abstract model (conformance testing). The test generation capability is limited and not scalable. In order to generate tests, the internal algorithm of Spec Explorer extracts a finite state machine (FSM) from ASM specifications and then use test generation techniques for FSMs. The effectiveness of their methodology is therefore severely constrained by the limits inherited from the use of Spec Explorer. The authors themselves say that the main difficulty is in using Spec Explorer and its methods for state space pruning and exploration. The ASMETA ATGT [Asmeta, 2007] tool that we intend to use for the same scope exploits, instead, the method of model checking to generate test sequences, and it is based on a direct encoding of ASMs in PROMELA, the language of the model checker SPIN [Holzmann, 1997].
The work in [Habibi & Tahar, 2006] also uses AsmL and Spec Explorer to settle a development and verification methodology for SystemC. They focus on assertion based verification of SystemC designs using the Property Specification Language (PSL), and although they mention test case generation as a possibility, the validation aspect is largely ignored. We were not able to investigate carefully their work as their tools are unavailable. Moreover, it should be noted that approaches in [Patel & Shukla, 2007;Habibi & Tahar, 2006], although using the Spec Explorer tool, do not exploit the scenario-based validation feature of Spec Explorer.
In [Mathaikutty et al., 2007], a model-driven methodology for development and validation of system-level SystemC designs is presented. The design flow is entirely based on the specification of a functional model (reference model) in the ESTEREL language, a state machine formalism, and on the use of the ESTEREL Studio development environment for the purpose of test generation. This approach provides coverage-directed test suite generation for system level design validation.
Authors in [Bruschi et al., 2005] provide test case generation by performing static analysis on SystemC designs. This approach is limited by the strength of the static analysis tools, and the lack of flexibility in describing the reachable states of interest for directed test generation. Moreover, static analysis requires sophisticated syntactic analysis and the construction of a semantic model, which for a language like SystemC (built on C++) is difficult due to the lack of formal semantics.
The SystemC Verification Library [OpenSystemCInitiative, 2008] is a standard for developing test-benches for SoC designs. It provides API for transaction-based verification, constrained and weighted randomization, exception handling, and HDL-connection. These techniques are applicable at SystemC code level, while we aim at developing formal techniques for validation of SystemC system designs at model level.