Formal Analysis of STM Design with SAL Infinite Bounded Model Checker

摘要

State Transition Matrix (STM) is a flexible table-like modeling language that has been frequently used for specifying behavior of distributed systems. In this paper, we first present a formalization of the static and dynamic aspects of a STM design (i.e., design written in STM). Consequentially, based on this formalization, we investigate how a STM design can be formally analyzed using SAL, precisely SAL infinite bounded model checker, through a language translation. Specifically, the formal analysis is conducted focusing on four kinds of safety properties related to: (1) Invalid Cells, (2) Static Constraints, (3) Dynamic Constraints, and (4) Deadlock, respectively, since the fulfillment of these properties is commonly desired by industrial practitioners for a STM design. A simple Internet Connection Control system is used as our demonstration example.