Author :
Wang, Dongfeng ; Ma, Hui ; Bastani, Farokh B. ; Yen, I-Ling
Author_Institution :
Dept. of Comput. Sci., Univ. of Texas at Dallas, Richardson, TX, USA
Abstract :
There are many applications that can be modeled as evolutions of continuous state spaces, such as real-time embedded systems, etc. For such applications, the divide-and-conquer method is usually used to achieve high quality software development. Instead of decomposing the state space based on phases, objects, etc., we decompose the state space based on aspects. Typically, there are four kinds of aspects, namely, constraint aspects, goal aspects, fairness aspects, and performance aspects. In our previous work (Bastini et al., 2001), we have investigated the decomposition of a system into constraint and goal aspects. In this paper, we further discuss the separation of fairness and performance aspects from constraint aspects and goal aspects, and the decomposition of fairness and performance aspects. All the decomposed aspects are guaranteed to be independently developable end-user assessable logical (IDEAL) aspects, meaning that each aspect can be designed and implemented independently, and can be tested or verified by the end user independently. Also, the system level properties (safety, stability, and reliability) can be inferred from the decomposed aspects mathematically to a high degree of confidence. A vehicle control system is used to illustrate the handling of the fairness and performance aspects in continuous process-control systems.
Keywords :
divide and conquer methods; embedded systems; process control; program verification; state-space methods; vehicles; IDEAL; continuous state spaces; formal verification; high-assurance continuous process-control systems; high-quality software development; independently developable end-user assessable logical; real-time embedded systems; vehicle control system; Application software; Control systems; Embedded system; Logic testing; Programming; Real time systems; Safety; Stability; State-space methods; Vehicles;