Critical systems require high reliability and are present in many domains. They are systems in which failure may result in financial damage or even loss of lives. Standard techniques of software engineering are not enough to ensure the absence of unacceptable failures and/or that critical requirements are fulfilled. Reo is a component-based modelling language that aims to provide a framework to build software based on existing pieces of software, which has been used in a wide variety of domains. Its formal semantics provides grounds to certify that systems based on Reo models satisfy specific requirements (i.e., absence of deadlocks). Current logical approaches for reasoning over Reo require the conversion of formal semantics into a logical framework. ReLo is a dynamic logic that naturally subsumes Reo's semantics. It provides a means to reason over Reo circuits. This work extends ReLo by introducing the iteration operator, and soundness and completeness proofs for its axiomatization.
翻译:重要系统需要具有高可靠性,出现在许多领域中。这些是可能导致财务损失甚至是生命丧失的故障出现时的系统。软件工程的标准技术不能保证不存在不可接受的故障和/或关键要求得到满足。Reo是一种基于组件的建模语言,旨在提供一个基于现有软件组件构建软件的框架,该语言已经被应用于多种域中。其形式化语义提供了认证基础,以便验证基于Reo模型的系统是否满足特定要求(例如消除死锁)。当前用于在Reo上进行推理的逻辑方法需要将其形式化语义转换为逻辑框架。ReLo是一种自然涵盖了Reo语义的动态逻辑。它提供了一种推理Reo电路的方法。这项工作通过引出迭代算子,并针对其公理化提供了声音和完备性证明,扩展了ReLo的功能。