Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Software and Systems Modeling
Published in: Software and Systems Modeling 2/2016

29-04-2014 | Regular Paper

Formalizing and verifying stochastic system architectures using Monterey Phoenix

Published in: Software and Systems Modeling | Issue 2/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The analysis of software architecture plays an important role in understanding the system structures and facilitate proper implementation of user requirements. Despite its importance in the software engineering practice, the lack of formal description and verification support in this domain hinders the development of quality architectural models. To tackle this problem, in this work, we develop an approach for modeling and verifying software architectures specified using Monterey Phoenix (MP) architecture description language. MP is capable of modeling system and environment behaviors based on event traces, as well as supporting different architecture composition operations and views. First, we formalize the syntax and operational semantics for MP; therefore, formal verification of MP models is feasible. Second, we extend MP to support shared variables and stochastic characteristics, which not only increases the expressiveness of MP, but also widens the properties MP can check, such as quantitative requirements. Third, a dedicated model checker for MP has been implemented, so that automatic verification of MP models is supported. Finally, several experiments are conducted to evaluate the applicability and efficiency of our approach
previous article Component-based verification using incremental design and invariants
next article View-based model-driven software development with ModelJoin

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
1
Without losing generality, we assume there is only one initial state in a PA.
 
2
Events and actions are interchangeable in this thesis.
 
Literature
1.
Allen, R., Douence, R., Garlan, D.: Specifying and analyzing dynamic software architectures. In: Astesiano, E. (ed) Fundamental Approaches to Software Engineering (FASE), vol. 1382, pp. 21–37. Springer, Berlin
2.
Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Trans. Softw. Eng. Methodol. 6(3), 213–249 (1997)CrossRef
3.
Auguston, M.: Monterey phoenix, or how to make software architecture executable. In: Arora, S., Leavens, G.T. (eds.) OOPSLA Companion, pp. 1031–1040. ACM, NY, USA (2009)
4.
Auguston, M.: Software architecture built from behavior models. ACM SIGSOFT Softw. Eng. Notes 34(5), 1–15 (2009)CrossRef
5.
Auguston, M., Whitcomb, C.: System architecture specification based on behavior models. In: Proceedings of the 15th ICCRTS Conference (International Command and Control Research and Technology Symposium), Santa Monica, CA, June 22–24 (2010)
6.
Baier, C., Katoen, J.: Principles of Model Checking. The MIT Press, Cambridge (2008)MATH
7.
Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/event-based software model checking. In: Leuschel, M., Wehrheim, H. (eds.) IFM, vol. 2999 of LNCS, pp. 128–147. Springer, Berlin (2004)
8.
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
9.
Corradini, F., Inverardi, P., Wolf, A.L.: On relating functional specifications to architectural specifications: a case study. Sci. Comput. Program. 59(3), 171–208 (2006)MathSciNetCrossRefMATH
10.
Garlan, D., Monroe, R.T., Wile, D.: Acme: an architecture description interchange language. In: Johnson, J.H. (ed.) CASCON, p. 7, IBM, Toronto (1997)
11.
12.
Inverardi, P., Wolf, A.L.: Formal specification and analysis of software architectures using the chemical abstract machine model. IEEE Trans. Softw. Eng. 21(4), 373–386 (1995)CrossRef
13.
Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002)CrossRef
14.
Kim, J.S., Garlan, D.: Analyzing architectural styles with alloy. In : Proceedings of the ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis, ROSATEA ’06, pp. 70–80. ACM, New York (2006)
15.
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV, Snowbird, vol. 6806, pp. 585–591, Springer, Heidelberg (2011)
16.
Liu, Y., Sun, J., Dong, J.S.: An analyzer for extended compositional process algebras. In: Schäfer, W., Dwyer, M.B., Gruhn, V. (eds.) ICSE Companion, pp. 919–920. ACM, Leipzig, Germany (2008)
17.
Liu, Y., Sun, J., Dong, J.S.: Pat 3:aAn extensible architecture for building multi-domain model checkers. In: Dohi, T., Cukic, B. (eds.) ISSRE, pp. 190–199. IEEE, Hiroshima, Japan (2011)
18.
Mahony, B.P., Dong, J.S.: Blending object-Z and timed CSP: an introduction to TCOZ. In: Proceedings of the 20th International Conference on Software Engineering (ICSE 1998), pp. 95–104 (1998)
19.
Pnueli. A.: The temporal logic of programs. In: Gruska, J. (ed.) FOCS, pp. 46–57. IEEE, Rhode Island, USA (1977)
20.
Roscoe., A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Englewood Cliffs (1997)
21.
Schrijver, A.: Combinatorial Optimization: Polyhedra and Efficiency. Springer, Berlin (2003)MATH
22.
Selvin, S.: On the monty hall problem (letter to the editor). Am. Stat. 29(3), 134 (1975)CrossRef
23.
Selvin, S.: A problem in probability (letter to the editor). Am. Stat. 29(1), 67–71 (1975)CrossRef
24.
Smith, G.: The Object-Z Specification Language. Kluwer Academic Publisher, Dordrecht (2000)CrossRefMATH
25.
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall Inc., Upper Saddle River (1989)MATH
26.
27.
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV, vol. 5643 of LNCS, pp. 709–714. Springer, Berlin (2009)
28.
Sun, J., Song, S.Z., Liu. Y.: Model checking hierarchical probabilistic systems. In: Dong, J.S., Zhu, H. (eds.) Formal Methods and Software Engineering, ICFEM, vol. 6447, pp. 388–403. Springer, Berlin (2010).
29.
Tan, L., Krings, A.: An adaptive N-variant software architecture for multi-core platforms: models and performance analysis. In: Proceedings of the International Conference on Computational Science and Its Applications, Part II (ICCSA’11), pp. 490–505 (2011)
30.
Zhang, J., Liu, Y., Auguston, M., Sun, J., Dong, J.S.: Using monterey phoenix to formalize and verify system architectures. In: Leung, K.R.P.H., Muenchaisri, P. (eds.) APSEC, pp. 644–653. IEEE, Hong Kong, China (2012)
31.
Zhang, P., Muccini, H., Li, B.: A classification and comparison of model checking software architecture techniques. J. Syst. Softw. 83(5), 723–744 (2010)CrossRef
Metadata
Title
Formalizing and verifying stochastic system architectures using Monterey Phoenix
Publication date
29-04-2014
Published in
Software and Systems Modeling / Issue 2/2016
Print ISSN: 1619-1366
Electronic ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-014-0411-7

Other articles of this Issue 2/2016

Software and Systems Modeling 2/2016 Go to the issue

Regular Paper

View-based model-driven software development with ModelJoin

Regular Paper

A framework for the operationalization of monitoring in business intelligence requirements engineering

Editorial

The evolution of model editors: browser- and cloud-based solutions

Regular Paper

ReFlO: an interactive tool for pipe-and-filter domain specification and program generation

Regular Paper

Heuristic search for equivalence checking

Special Section Paper

Effective application of process improvement patterns to business processes

Premium Partner

    Image Credits