On Detecting Concurrency Defects Automatically at the Design Level
We describe an automated approach for detecting concurrency defects from design diagrams of a software, in particular, sequence diagrams. From a given sequence diagram, we automatically infer a formal, parallel specification that generalizes the communication behavior that is designed informally and incompletely in the diagram. We model-check the parallel specification against generic concurrency defect patterns. No additional specification of the software is needed. We present several case-studies to evaluate our approach. The results show that our approach is technically feasible, and effective in detecting nasty concurrency defects at the design level.
|Zugehörige Institution(en) am KIT
||Institut für Programmstrukturen und Datenorganisation (IPD)
KITopen ID: 1000055667
||20th Asia-Pacific Software Engineering Conference (APSEC 2013), Bangkok, Thailand, 2 - 5 December 2013 ; [proceedings]
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page