| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 6870861 | Computer Languages, Systems & Structures | 2018 | 30 Pages |
Abstract
SAwUML is supported with a modelling tool for specifying the structural and behavioural design decisions together and any system-level properties in the linear temporal logic. The tool can automatically translate the software architectures in SAwUML into a formal ProMeLa model. Then the SPIN model checker can be used to verify the resulting ProMeLa models for the pre-defined properties - i.e., deadlock and incompleteness - and any user-defined properties.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Mert Ozkaya, Mehmet Alp Kose,