Design for Independent Composition and Evaluation of High-Confidence Embedded Software Systems

Embedded computer systems are systems in which one or more computers monitor and control a larger electromechanical system. Applications include telecommunication systems, health care systems, defense systems, manufacturing automation systems, etc. Many of these systems have mission-critical requirements and, hence, it is necessary to have high confidence in their reliability before deploying them. Further, due to variable environmental conditions and rapid technological advances, it is necessary to design these systems to be adaptable and easily modifiable. One way of achieving these objectives is to decompose a complex system into smaller subsystems. Several decomposition methods have been developed. However, most of these methods do not necessarily enable system properties to be inferred from subsystem properties. In this paper, we constrain each subsystem to be an Independently Developable and End-user Assessable Logical (IDEAL) subsystem. We classify a system of IDEAL subsystems into three classes depending on the interaction pattern among the subsystems. Then, we present an extended finite state machine notation for modeling these subsystems and show how they can be statically composed together to form the system. The paper also shows how system-level properties can be computed from IDEAL subsystem-level properties. Keywords: Embedded software systems, High-assurance methods, Software decomposition and composition, Software reliability assessment