An ASTRAL-Based Support Environment for Formal Software Development of Realtime Systems

该合同解决了通过更好的软件开发方法和工具，特别是通过将正式方法应用于实时系统开发来提高系统可靠性的需求。所寻求的解决方案是一个规范和分析实时系统的正式框架。该框架以ASTRAL形式规范语言为基础，包括用于编写实时系统需求和设计规范的ASTRAL语言，用于证明ASTRAL规范特性的形式证明理论，以及用于构建和分析规范的支持环境。组成支持环境的工具是一个语法导向的编辑器、一个ASTRAL到TRIO的转换器、一个ASTRAL规范处理器和一个力学定理证明器。由米兰理工大学开发的基于trio的模型检查器正在集成到支持环境中。要研究的主要理论问题是ASTRAL规范的可组合性。该研究正在开发一种证明理论，该理论规定了如何将单个状态机规范的证明组合起来以产生整个系统的证明。要研究的另一个可组合性问题是组合两个或多个ASTRAL系统规范（即，一个全局规范及其相关的状态机规范集合），以派生出组合系统的规范。ASTRAL被用于从各种应用领域指定复杂的实时系统，以评估其有效性和效用。

This award addresses the need for improving system reliability through better software development methods and tools, and specifically, through applying formal methods to the development of realtime systems. The solution sought is a formal framework for the specification and analysis of realtime systems. This framework is based on the ASTRAL formal specification language and includes the ASTRAL language for writing requirements and design specifications of realtime systems, a formal proof theory for proving properties about ASTRAL specifications, and a support environment for the construction and analysis of the specifications. The tools that make up the support environment are a syntax-directed editor, an ASTRAL to TRIO translator, an ASTRAL specification processor, and a mechanical theorem prover. The TRIO-based model checkers, developed at the Politecnico di Milano, are being integrated into the support environment. The main theoretical issues to be investigated deal with the composability of ASTRAL specifications. The research is developing a proof theory that prescribes how the proofs of the individual state machine specifications can be combined to produce a proof of the entire system. Another composability issue to be investigated is the composition of two or more ASTRAL system specifications (i.e., a global specification and its associated collection of state machine specifications) to derive the specification for the composite system. ASTRAL is being used to specify complex realtime systems taken from a variety of application areas to evaluate its effectiveness and utility.