Symbolic Execution of Behavioral Requirements

10 years 2 months ago
Symbolic Execution of Behavioral Requirements
Message Sequence Charts (MSC) have traditionally been used as a weak form of behavioral requirements in software design; they denote scenarios which may happen. Live Sequence Charts (LSC) extend Message Sequence Charts by also allowing the designer to specify scenarios which must happen. Live Sequence Chart specifications are executable; their simulation allows the designer to play out potentially aberrant scenarios prior to software construction. In this paper, we propose the use of Constraint Logic Programming (CLP) for symbolic execution of requirements described as Live Sequence Charts. The utility of CLP stems from its ability to execute in the presence of uninstantiated variables. This allows us to simulate multiple scenarios at one go. For example, several scenarios which only differ from each other in the value of a variable may be executed as a single scenario where the variable is left uninstantiated. Similarly, we can simulate scenarios with an unbounded number of processe...
Tao Wang, Abhik Roychoudhury, Roland H. C. Yap, S.
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where PADL
Authors Tao Wang, Abhik Roychoudhury, Roland H. C. Yap, S. C. Choudhary
Comments (0)