Analyzing partially-implemented real-time systems

作     者：Avrunin, GS Corbett, JC Dillon, LK 

作者机构：Univ Massachusetts Dept Math & Stat Amherst MA 01003 USA Univ Hawaii Dept Informat & Comp Sci Honolulu HI 96822 USA Michigan State Univ Dept Comp Sci & Engn E Lansing MI 48824 USA 

出 版 物：《IEEE TRANSACTIONS ON SOFTWARE ENGINEERING》 (IEEE Trans Software Eng)

年 卷 期：1998年第24卷第8期

页      面：602-614页

核心收录：

学科分类：0808[工学-电气工程] 08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：University of California and Hughes Electronics Corporation, (UCM-20880) National Science Foundation, NSF, (CCR-9308067, CCR-9407182, CCR-9505392, CCR-9708184) Defense Advanced Research Projects Agency, DARPA, (F30602-94-C-0137) Air Force Materiel Command, AFMC Rome Laboratory 

主　　题：real-time concurrency static analysis Ada temporal logic hybrid systems Graphical Interval Logic 

摘      要：Most analysis methods for real-time systems assume that all the components of the system are at roughly the same stage of development and can be expressed in a single notation, such as a specification or programming language. There are, however, many situations in which developers would benefit from tools that could analyze partially-implemented systems, those for which some components are given only as high-level specifications while others are fully implemented in a programming language. In this paper, we propose a method for analyzing such partially-implemented real-time systems. Here we consider real-time concurrent systems for which some components are implemented in Ada and some are partially specified using regular expressions and Graphical Interval Logic (GIL), a real-time temporal logic. We show how to construct models of the partially-implemented systems that account for such properties as run-time overhead and scheduling of processes, yet support tractable analysis of nontrivial programs. The approach can be fully automated, and we illustrate it by analyzing a small example.