Design and Analysis Support for Abstract Models of Component-based Embedded Systems

Developing industrial real-time software systems is challenging due to demands on system safety and reliability, through stringent system requirements in terms of functionality, timing, resource consumption etc. Due to this, the system development needs to ensure predictability before the actual implementation, through reliable engineering methods. To address these challenges, model-based engineering (MBE) combined with Component-based development (CBD) has emerged as a feasible solution. MBE supports system modeling and formal analysis through the development phases such as requirements, specification, and design. CBD supports reusability of software parts leading to faster development time, and reduced costs. However, an integrated approach needs to deal with various abstractions of the system during different phases of the development. In this thesis, we present model-based techniques, for the development of predictable, component-based designs of embedded systems. We consider ProCom as the underlying component model and, as a first step, we define a formal semantics for its architectural elements. The given semantics provides a basis for developing analyzable embedded systems designs, associated analysis techniques, model transformations etc. Next, we describe some commonly-found behavioral patterns, in component-based designs. These patterns provide an abstract, and reusable specification of a real-time component’s functionality. Also, we define component-based design templates, intended to support the systematic development of component-based designs from abstract system models. Finally, we propose a formal framework to correlate statemachine-based system behavior with corresponding ProCom-based system designs. We validate our research contributions using case-studies and examples, and also by applying verification techniques, such as, model-checking.