NDLI: Formalizing and verifying stochastic system architectures using Monterey Phoenix

Content Provider	Springer Nature Link
Author	Song, Songzheng Zhang, Jiexin Liu, Yang Auguston, Mikhail Sun, Jun Dong, Jin Song Chen, Tieming
Copyright Year	2014
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
Starting Page	453
Ending Page	471
Page Count	19
File Format	PDF
ISSN	16191366
Journal	Software and Systems Modeling
Volume Number	15
Issue Number	2
e-ISSN	16191374
Language	English
Publisher	Springer Berlin Heidelberg
Publisher Date	2014-04-29
Publisher Place	Berlin, Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Model checking Stochastic system architecture Monterey Phoenix Software Engineering/Programming and Operating Systems Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters Information Systems Applications (incl. Internet) IT in Business
Content Type	Text
Resource Type	Article
Subject	Modeling and Simulation Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Constructing and verifying a robust Mix Net using CSP

Heuristic search for equivalence checking

Model-checking software library API usage rules

Domain specific modeling

Introductory paper

Model aesthetics

A survey of approaches for verifying model transformations

Models for digitalization

Least privilege analysis in software architectures

Formalizing and verifying stochastic system architectures using Monterey Phoenix

Similar Documents

Constructing and verifying a robust Mix Net using CSP

Heuristic search for equivalence checking

Model-checking software library API usage rules

Domain specific modeling

Introductory paper

Model aesthetics

A survey of approaches for verifying model transformations

Models for digitalization

Least privilege analysis in software architectures

Formalizing and verifying stochastic system architectures using Monterey Phoenix