Specification guidelines to avoid the state space explosion problem. (12th May 2014)

• Record Type: Journal Article
• Authors: Groote, Jan Friso; Kouters, Tim W.D.M.; Osaiweran, Ammar
• Is Part Of: Software testing, verification & reliability. Volume 25:Number 1(2015:Jan.)
• Page Start: 4
• Page End: 33
• Publication Date: 2014-05-12
• Subjects: Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1536
• Languages: English
• ISSNs: 0960-0833

Abstract

<abstract abstract-type="main" id="stvr1536-abs-0001"> <title>SUMMARY</title> <p id="stvr1536-para-0001">During the last two decades, we modelled the behaviour of a large number of systems. We noted that different styles of modelling had quite an effect on the size of the state spaces of the modelled systems. The differences were so substantial that some specification styles led to far too many states to verify the correctness of the model, whereas with other styles, the number of states was so small that verification was a straightforward activity. In this article, we summarize our experience by providing seven specification guidelines to keep state spaces small. For each guideline, we provide an application, generally from the realm of traffic light controllers, for which we provide a 'bad' model with a large state space, and a 'good' model with a small state space. The good and bad models are both suitable for their purpose but are <italic>not</italic> behaviourally equivalent. For all guidelines, we discuss circumstances under which it is reasonable to apply the guidelines. Copyright © 2014 John Wiley &amp; Sons, Ltd.</p> </abstract>