Sciweavers

EMSOFT
2011
Springer

Model-checking behavioral programs

12 years 3 months ago
Model-checking behavioral programs
System specifications are often structured as collections of scenarios and use-cases that describe desired and forbidden sequences of events. A recently proposed behavioral programming approach, which evolved from the visual language of live sequence charts (LSCs), calls for coding software modules in alignment with such scenarios. We present a methodology and a supporting model-checking tool for verifying behavioral Java programs, without having to first translate them into a specific input language for the model checker. Our method facilitates early discovery of conflicting or under-specified scenarios, which can often be resolved by adding new scenarios rather than by changing existing code. Also, counterexamples provided by the tool are themselves event sequences that can serve directly for refinements and corrections. Our tool reduces the size of the execution ace using an abstraction that focuses on behaviorally interesting states and treats transitions between them as ato...
David Harel, Robby Lampert, Assaf Marron, Gera Wei
Added 20 Dec 2011
Updated 20 Dec 2011
Type Journal
Year 2011
Where EMSOFT
Authors David Harel, Robby Lampert, Assaf Marron, Gera Weiss
Comments (0)