Synchronous model is a type of formal models for modelling and specifying reactive systems. It has a great advantage over other real-time models that its modelling paradigm supports a deterministic concurrent behaviour of systems. Various approaches have been utilized for verification of synchronous models based on different techniques, such as model checking, SAT/SMT sovling, term rewriting, type inference and so on. In this paper, we propose a verification approach for synchronous models based on compositional reasoning and term rewriting. Specifically, we initially propose a variation of dynamic logic, called synchronous dynamic logic (SDL). SDL extends the regular program model of first-order dynamic logic (FODL) with necessary primitives to capture the notion of synchrony and synchronous communication between parallel programs, and enriches FODL formulas with temporal dynamic logical formulas to specify safety properties -- a type of properties mainly concerned in reactive systems. To rightly capture the synchronous communications, we define a constructive semantics for the program model of SDL. We build a sound and relatively complete proof system for SDL. Compared to previous verification approaches, SDL provides a divide and conquer way to analyze and verify synchronous models based on compositional reasoning of the syntactic structure of the programs of SDL. To illustrate the usefulness of SDL, we apply SDL to specify and verify a small example in the synchronous model SyncChart, which shows the potential of SDL to be used in practice.
翻译:同步模型是建模和指定反应系统的一种正式模型类型。 它与其他实时模型相比有很大的优势, 它的建模模式模式支持了确定性同步的系统行为。 已经利用了不同方法核查基于不同技术的同步模型, 如模型检查、 SAT/ SMT Soving、 术语重写、 字型重写、 类型推论等。 在本文中, 我们提议了一种基于组成推理和术语重写的同步模型的核查方法。 具体地说, 我们最初提出了一种动态逻辑的变异, 叫做同步动态逻辑( SDL)。 SDL 扩展了一级动态逻辑( FODL) 的常规程序模型, 以必要的原始程序来捕捉同步和同步交流的概念, 并用时间动态逻辑公式来丰富FODL 公式, 以指定安全特性 -- -- 一种主要与反应系统有关的特性类型。 为了正确捕捉同步的通信, 我们为SDL 程序模型定义了一种建设性和相对完整的校准系统。 我们为SDL 的SDL 的SDL 的同步模型构建了一个正确和相对完整的校验样系统, 校验SDL 的校验SDL 的模型的校验方法, 的比了SDL 的SDL 和SDL 的校正的校正的校正的校正的校正的校正的校正的校正的校正的校正的校正的校正的模型, 和校正的校正的校正的校正的校正的校正的模型, 的校正的校正的校正的校正的校正的校正的校正和制和校正的校正的校正和校正的校正的校正的校正的校正的校正的校正的校正方法, 。