Specifying UML protocol state machines in Alloy
| Autor: | Ana C. R. Paiva, Ana Gabriela Garis, Daniel Eduardo Riesco, Alcino Cunha |
|---|---|
| Přispěvatelé: | Universidade do Minho |
| Jazyk: | angličtina |
| Rok vydání: | 2012 |
| Předmět: |
Computer science
Model transformation Applications of UML Protocol state machines 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences Software development process Unified Modeling Language 0202 electrical engineering electronic engineering information engineering Requirements analysis Object Constraint Language computer.programming_language UML tool Finite-state machine Programming language business.industry Software development 020207 software engineering OCL Formal methods UML 010201 computation theory & mathematics Alloy business computer Verification and validation |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783642307287 IFM |
| Popis: | 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. Fundação para a Ciência e a Tecnologia |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|