An approach for modeling and analyzing dynamic software architectures

摘要

Software architectures define the overall structure of software systems as composition of interacting components connecting through connectors. As the foundation to the development of software systems, the correctness of the software architecture is critical to the quality of the final product. Formally modeling and analyzing software architectures is an effective way to ensure the correctness of the software architecture. Many formal specification and analysis approaches have been proposed during past three decades. However, the focus of the majority of the approaches is on the static software architecture, which doesn't change the composition of components during a computation. As cloud computing has been widely adopted as a new computing paradigm, the dynamic software architecture that changes the composition of components during a computation becomes an important research topic. Although research work on specification and analysis of dynamic software architectures was published 20 years ago, building current distributed systems requires better scalability and usability for the modeling and analysis approach. In this paper, the software architecture is modelled using a two-layer higher Petri nets extended with communication channels called CPrT. CPrT nets model static and dynamic software architectures using a uniform formal notation. Its graph notation is easy to use and its executable is necessary for developers to build complex models. Its communication channels that are used for modeling the dynamic composition of software architectures implement the channels in pi-calculus. The semantics of CPrT nets can be described through transforming them into regular Petri nets. The analysis of CPrT nets is conducted using model checking with its tool SPIN.