2017/04/24 by Chih-Hong Cheng, Chih‐Hong Cheng, Yassine Hamza +5
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Model-Driven Software Engineering Techniques #Software Engineering (cs.SE) #cs.LO #cs.SE
paper · pdf · doi:10.48550/arxiv.1704.07097
Timestamping research work conducted under the fortiss Eigenforschung project
arxiv created 2017/04/24 · openalex publication_date 2017/04/24 · arxiv updated 2017/04/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Software architectures usually are comprised of different views for capturing static, runtime, and deployment aspects. What is currently missing, however, are formal validation and verification techniques of multi-view architecture in very early phases of the software development lifecycle. The main contribution of this paper therefore is the construction of a single formal model (in Promela) for certain stylized, and widely used, multi-view architectures by suitably interpreting and fusing sub-models from different UML diagrams. Possible counter-examples produced by model checking are fed back as test scenarios for debugging the multi-view architectural model. We have implemented this algorithm as a plug-in for the Enterprise Architect development tool, and successfully used SPIN model checking for debugging some industrial architectural multi-view models by identifying a number of undesirable corner cases.