Software architectural modelling and verification: a Petri net and temporal logic approach

Abstract

Component-based software development has been well recognized as an effective methodology in software engineering. Components’ constraints play a critical role in high-quality software product development. In this paper we present a systematic approach for component-based software architectural modelling, constraints specification and consistency verification. In this approach, computational tree logic and Petri Nets are used as the underlying formalisms to describe software constraints and design compositions, respectively. System-wide constraints are decomposed to component constraints. The consistency between system-wide constraints and component constraints are verified purely on Petri net models after replacing black-box components with equivalent Petri nets while preserving component properties specified by the constraints. An example is used throughout the paper to illustrate the approach.

Keywords

constraints Petri nets software architecture software components temporal logic.

Get full access to this article

View all access options for this article.

References

Clarke, E.M. , Grumberg, O. and Peled, D. 1999: Model checking. The MIT Press.

Crnkovic, I. , Larsson, S. and Stafford, J. 2002: Component-based software engineering: building systems from components. ACM SIGSOFT Software Engineering Notes 27, 47-50.

Deng, Y. , Wang, J. , Tsai, J. and Beznosov, K. 2003: An approach for modeling and analysis of security system architectures. IEEE Transactions on Knowledge and Database Engineering 15, 1099-119.

Deng, Y. , Wang, J. , He, X. and Tsai, J. 2004: Constraint propagation and progressive verification for component-based process model. International Journal of Software Engineering and Knowledge Engineering 14, 471-96.

Emerson, E.A. , Mok, A.K. , Sistla, A.P. and Srinivasian, J. 1992: Quantitative temporal reasoning. Concurrent Systems 4, 331-52.

Graham, I. 1995: Migrating to object technology. Addison-Wesley .

Huth, M. and Ryan, M. 2004: Logic in computer science: modeling and reasoning about systems. Cambridge University Press.

Reisig, W. 1985: Petri nets - an introduction. Springer-Verlag .

Rumbaugh, J. , Jacobson, I. and Booch, G. 1999: The unified modeling language reference manual. Addison-Wesley.

10.

Thuraisingham, B. and Ford, W. 1995: Security constraint processing in a multilevel secure distributed database management system. IEEE Transactions on Knowledge and Data Engineering 7, 274-93.

11.

Warmer, J. and Kleppe, A. 1999: The object constraint language - precise modeling with UML. Addison-Wesley.

12.

Wang, J. 1998: Timed Petri nets: theory and application. Kluwer Academic.

13.

Wang, J. , Deng, Y. and Xu, G. 2000: Reachability analysis of concurrent systems based on time Petri nets. IEEE Transactions on Systems, Man and Cybernatics B 30, 725-36.