Specifying UML protocol state machines in alloy

• Type: Article in International Conference Proceedings Book
• Date: 2012

Authors

Ana Garis (Author) Other; Ana C. R. Paiva (Author) FEUP; Alcino Cunha (Author) Other; Daniel Riesco (Author) Other

Conference proceedings International

Title: IFM

Pages: 312-326

Integrated Formal Methods - 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings

Indexing

ISI Web of Knowledge

Scopus - 8 Citations

Other information

Authenticus ID: P-008-58P

DOI: 10.1007/978-3-642-30729-4_22

Abstract (EN): A UML Protocol State Machine (PSM) is a behavioral diagram for the specification of the external behavior of a class, interface or component. PSMs have been used in the software development process for different purposes, such as requirements analysis and testing. However, like other UML diagrams, they are often difficult to validate and verify, specially when combined with other artifacts, such as Object Constraint Language (OCL) specifications. This drawback can be overcome by application of an off-the-shelf formal method, namely one supporting automatic validation and verification. Among those, we have the increasingly popular Alloy, based on a simple relational flavor of first-order logic. This paper presents a model transformation from PSMs, optionally complemented with OCL specifications, to Alloy. Not only it enables automatic verification and validation of PSMs, but also a smooth integration of Alloy in current software development practices. © 2012 Springer-Verlag.

Language: English

Type (Professor's evaluation): Scientific