Journals / Havacılık ve Uzay Teknolojileri Dergisi / 2020 / Cilt: 13 - Sayı: 2
Yazılım Mimarilerinin Genel-amaçlı olarak Modellenmesi, Analizi, ve Koda Dönüştürülmesi
- Pages
- 165–177
- DOI
- —
Abstract
Bu makalede, endüstride sıklıkla kullanılan UML modelleme dilinden esinlenen SAMP adında yeni bir yazılım mimarisi modelleme dili önerilmektedir. SAMP ile, modellenen yazılım mimarileri, biçimsel yöntemler kullanılarak analiz edilebilir, ve sonrasında otomatik olarak koda dönüştürülebilir. SAMP, yazılım mimarilerinin gereksinim, mantıksal, davranışsal, ve fiziksel bakış açılarına göre ayrı ayrı modellenebilmesini desteklemektedir. Ayrıca, bir araç kümesi aracılığıyla, SAMP modelleri otomatik olarak ProMeLa biçimsel sınama dilinde modellere dönüştürülerek ProMeLa’yı destekleyen SPIN model sınayıcısıyla kapsamlı olarak analiz edilebilir ve kullanıcı-tanımlı ve önceden-tanımlı birçok özelliğin sağlanıp sağlanmadığı anlaşılabilir. Yine aynı araç desteği ile, analiz edilen modeller Java Modeling Language (JML) dilinde koda dönüştürülebilir. JML sayesinde, model ile Java kodunu bir arada yürütmek mümkün olup kodun modeli sağlayıp sağlamadığı JML’i destekleyen araçlar ile sürekli test edilebilir.
Özet
In this paper, a new software modeling language called SAMP is proposed, which is inspired from UML and enables the general-purpose modeling of software architectures but at the same time promotes the multiple-viewpoints modeling, formal verification of the models for the desired requirements, and combining model and code together. SAMP supports the high-level modeling of software architectures from the requirements, logical, behavioral, and deployment perspectives and supports checking the consistencies between the software models in different perspectives. SAMP is also supported with a modeling toolset that allows for the visual modeling of software architectures in those perspectives. The toolset further generates formal ProMeLa models that can be accepted by the SPIN model checker for the exhaustive verification of the software behaviors against the user-defined properties and some pre-defined properties (e.g., deadlock, race-condition, wrong and incomplete preconditions). Moreover, the toolset can also generate the Java Modeling Language (JML) code that combines the contractual models with the Java program for ensuring the consistency between model and code throughout the software development.