SAwUML - UML-based, contractual software architectures and their formal analysis using SPIN
[ X ]
Tarih
2018
Yazarlar
Dergi Başlığı
Dergi ISSN
Cilt Başlığı
Yayıncı
Pergamon-Elsevier Science Ltd
Erişim Hakkı
info:eu-repo/semantics/closedAccess
Özet
UML is without doubt the top preferred software modelling language by practitioners. However, UML remains inadequate for the software architecture level of design due to its weak support for some important requirements including multiple viewpoints, connectors, and formal analysis. In this paper, the SAwUML architecture description language is proposed to improve UML for the high-level, precise specifications of the structural and behavioural design decisions and their formal analysis. To this end, SAwUML combines UML's component and sequence diagrams together under the same notation set. Using the component diagram, practitioners can specify their system components that are connected via the required and provided ports and interact over the port method-calls. Whenever a component port is clicked, a UML sequence diagram can be drawn for specifying the port methods in terms of the request and response messages that are exchanged between the interacting components. SAwUML extends the formal Design-by-Contract approach for the behaviour specifications of the port methods drawn in the sequence diagram. SAwUML's contract extension considers both the request and response messages of method-calls, deciding on when method-calls can be requested/received, the method parameters/results to be assigned, and how the component post-state should be after method-calls. 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. (C) 2018 Elsevier Ltd. All rights reserved.
Açıklama
Ozkaya, Mert/0000-0003-2329-9925; Ozkaya, Mert/0000-0002-3464-6489
Anahtar Kelimeler
Software Architecture, UML, Design-by-Contract, ProMeLa, Formal Verification
Kaynak
Computer Languages Systems & Structures
WoS Q Değeri
N/A
Scopus Q Değeri
N/A
Cilt
54
