Analyzing Behavioural Scenarios over Tabular Specifications Using Model Checking

Abstract

Tabular notations, in particular SCR specifications, have proved to be a useful means for formallydescribing complex requirements. The SCR method offers a powerful family of analysis tools, knownas the SCR Toolset, but its availability is restricted by the Naval Research Laboratory of USA. Thistoolset applies different kinds of analysis considering thewholeset of behaviours associated with arequirements specification.In this paper we present a tool for describing and analyzing SCR requirements descriptions, thatcomplements the SCR Toolset in two aspects. First, its use is not limited by any institution, and re-sorts to a standard model checking tool for analysis; and second, it allows to concentrate the analysisto particular sets of behaviours (subsets of the whole specifications), that correspond to particularscenarios explicitly mentioned in the specification.We take an operational notation that allows the engineer to describe behavioural “scenarios” bymeans of programs, and provide a translation into Promela to perform the analysis via Spin, anefficientoff-the-shelfmodel checker freely available. In addition, we apply the SCR method to aPacemakersystem and we use its tabular specification as a running example of this article.