A Formal Approach for Component Based Embedded Software Modelling and Analysis
Hyggo Oliveira de Almeida, Leandro Dias da Silva, Eugénio Oliveira, Ângelo Perkusich · 2005
To develop software for embedded systems the designer must take into account different kinds of problems and complexities. The main issues are related to late inte- gration with the target hardware and the separation of the development environments from target execution platforms. Due to the fact that in most situations they are developed using low-level programming languages, approaches to de- velop complex software systems, such as component based software development, cannot be used at all. In this work we introduce a component based development process that integrates colored Petri nets and a component model in order to introduce better abstraction mechanisms in the modelling, analysis and verification processes for embedded software systems. I. INTRODUCTION Embedded systems software has been increased in complexity in the last years. Component based software development (CBSD) is a key approach to deal with such complexity. However, most of the component models are targeted to desktop computers, with abundant hardware re- sources managed by high level operating systems, making available a high level abstraction programming model. On the other hand, embedded software has specific problems and complexities to be considered, such as late integration with the target hardware and separate environments for development and target execution. Therefore, it is neces- sary to define and adopt abstraction techniques, theories, and tools to develop embedded software. Also, the life- cycle to develop software for embedded systems must be shorter than for desktop applications, and the development process must address the constant changes in hardware in a safe, and controlled way, but still considering the time to market. In order to deal with these constraints, concepts such as product lines (1), software architectures (2), and components (3), have been applied to promote the adop- tion of the development processes to allow the assembly of systems based on a framework and a set of components. Thus, common components of entities or functionalities previously developed can be reused, and a cheaper and faster development process can be used, thus resulting in more dependable embedded software. On the other hand, to ensure high availability, the devel- opment process for embedded software must address qual- ity requirements. In this context, validation techniques, such as formal modelling, simulation and model checking, are becoming essential (4). The use of formal methods to model systems aggregates