SAwUML - UML-based, contractual software architectures and their formal analysis using SPIN

Basit Öğe Kaydı
dc.contributor.authorÖzkaya, Mert
dc.contributor.authorKöse, Mehmet Alp
dc.date.accessioned2021-05-15T12:41:31Z
dc.date.available2021-05-15T12:41:31Z
dc.date.issued2018
dc.departmentMühendislik ve Doğa Bilimleri Fakültesi, Bilgisayar Mühendisliği Bölümüen_US
dc.descriptionOzkaya, Mert/0000-0003-2329-9925; Ozkaya, Mert/0000-0002-3464-6489
dc.description.abstractUML 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.en_US
dc.identifier.doi10.1016/j.cl.2018.04.005
dc.identifier.endpage94en_US
dc.identifier.issn1477-8424
dc.identifier.issn1873-6866
dc.identifier.scopus2-s2.0-85047059017
dc.identifier.scopusqualityN/A
dc.identifier.startpage71en_US
dc.identifier.urihttps://doi.org/10.1016/j.cl.2018.04.005
dc.identifier.urihttps://hdl.handle.net/20.500.12939/815
dc.identifier.volume54en_US
dc.identifier.wosWOS:000454970200004
dc.identifier.wosqualityN/A
dc.indekslendigikaynakWeb of Science
dc.indekslendigikaynakScopus
dc.institutionauthorÖzkaya, Mert
dc.institutionauthorKöse, Mehmet Alp
dc.language.isoen
dc.publisherPergamon-Elsevier Science Ltden_US
dc.relation.ispartofComputer Languages Systems & Structures
dc.relation.publicationcategoryMakale - Uluslararası Hakemli Dergi - Kurum Öğretim Elemanıen_US
dc.rightsinfo:eu-repo/semantics/closedAccessen_US
dc.subjectSoftware Architectureen_US
dc.subjectUMLen_US
dc.subjectDesign-by-Contracten_US
dc.subjectProMeLaen_US
dc.subjectFormal Verificationen_US
dc.titleSAwUML - UML-based, contractual software architectures and their formal analysis using SPIN
dc.typeArticle

Dosyalar

Koleksiyon

WoS İndeksli Yayınlar Koleksiyonu
Bilgisayar Mühendisliği Bölümü Koleksiyonu
Scopus İndeksli Yayınlar Koleksiyonu