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...

• Type: Conference
• Year: 2004
• Where: PADL
• Authors: Tao Wang, Abhik Roychoudhury, Roland H. C. Yap, S. C. Choudhary
• Keywords: Live Sequence Charts, PADL 2004, Programming Languages, Scenarios, Sequence Charts