Multi-parameterised compositional verification of safety properties

详细信息    查看全文

• 作者：Antti Siirtola^a ; ¹ ; ^{antti.siirtola@aalto.fi" class="auth_mail" title="E-mail the corresponding author} ; ^{antti.siirtola@oulu.fi" class="auth_mail" title="E-mail the corresponding author} ; Juha Kortelainen^b ; ^{juha.kortelainen@oulu.fi" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Parameterised verification ; Refinement checking ; Concurrency theory ; Compositional reasoning ; Decidability
• 刊名：Information and Computation
• 出版年：2015
• 出版时间：October 2015
• 年：2015
• 卷：244
• 期：Complete
• 页码：23-48
• 全文大小：872 K

文摘

We introduce a fully automatic technique for the parameterised verification of safety properties. The technique combines compositionality and completeness with support to multiple parameters and it is implemented in a tool. We start with an LTS-based (Labelled Transition System) CSP-like (Concurrent Sequential Processes) formalism with parallel composition and hiding operators. First, we equip the formalism with types and variables which enable parameterising the structure of a system and prove that the formalism remains compositional. Next, we show how trace refinement between parameterised processes can be checked by computing structural cut-offs for types. This way, a parameterised verification task reduces to finitely many finite state refinement checks. We also provide an extension to the theory which allows for user definable universal relations. This enables parameterising system topology to some extent, too. Finally, we consider the assumptions related to the approach and show that each of them is necessary for decidability.