Formal verification of real-time embedded software in an object-oriented application framework
Formal verification of real-time embedded software in an object-oriented application framework
复制标题
面向对象应用框架中实时嵌入式软件的形式化验证
DOI：
10.1049/ip-cdt:20041102
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Win
中科院分区：
文献类型：
--
作者：
Pao;Trong;Jih;Win
随着实时嵌入式软件设计复杂性的快速升级，应用程序框架已经成为几乎不可或缺的工具，因为它们通过代表设计人员执行繁琐的任务和通过重用半完整的应用程序代码，极大地简化了设计人员的工作。为了保证代码的质量和可靠性，在一些框架下对生成的应用软件进行了计算机辅助分析。然而，当目标是实时嵌入式系统时，软件在满足所有用户给定的实时和嵌入式约束方面的正确性成为这些框架的主要目标。为了保证正确性，模型检查形式的形式化验证是一种可行的解决方案，因为它具有完全自动化的能力。然而，从现有的文献或工业经验中，很少有人知道如何将形式验证集成到面向对象的应用程序框架中，其主要目的以前只是为了设计和生成应用程序软件。这项工作通过展示如何集成设计框架和验证框架，为最先进的技术做出了贡献。解决了三个主要问题：(i)核查什么？（ii）何时核实？（三）如何验证？为了解决这三个问题，作者分别提出了一种从面向对象模型到形式化模型的映射、一种进度-验证-映射策略和一种组合验证方法。在基于组件的框架中实现了这些功能，并进行了实验以说明其可行性。由于结合了行业实际标准，例如实时统一建模语言和实时Java，在提议的技术中，工程师现在应该可以获得理论上证明的正式验证技术，否则，对于不熟悉验证技术的工程师来说，这些技术将被认为是无法访问的。
With the rapid escalation in design complexity of real-time embedded software, application frameworks have become an almost indispensable tool because they greatly ease the work of a designer by performing tedious tasks on behalf of a designer and by reusing semi-complete application codes. To ensure code quality and reliability, computer-aided analysis is also performed for the generated application software in some frameworks. However, when the target is real-time embedded systems, the correctness of the software in terms of satisfying all user-given real-time and embedded constraints becomes a primary objective for such frameworks. To guarantee correctness, formal verification in the form of model checking is a viable solution due to its full automation capability. Nevertheless, little is known from either the existing literature or industrial experience on how formal verification can be integrated into an object-oriented application framework, whose primary purpose was previously only to design and generate application software. This work contributes to the state-of-art technology by showing how a design framework and a verification framework can be integrated. Three main issues are tackled: (i) what to verify?; (ii) when to verify?; and (iii) how to verify? As a solution to these three issues the authors propose a mapping from the object-oriented model to a formal model, a schedule-verify-map strategy and a compositional verification methodology, respectively. These have been implemented in a component-based framework and experiments performed to illustrate their feasibility. Due to the incorporation of industry de-facto standards such as real-time unified modelling language and real-time Java, in the proposed techniques it should now be possible for an engineer to gain access to theoretically proven formal verification technologies that would otherwise be considered to be inaccessible to an engineer unskilled in verification techniques.