Formalizing and verifying stochastic system architectures using Monterey Phoenix
Dong, Jin Song
MetadataShow full item record
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.
The article of record as published may be found at http://dx.doi.org/10.1007/s10270-014-0411-7
RightsThis publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.
Showing items related by title, author, creator and subject.
Pace, Kyongsuk P. (Monterey, California. Naval Postgraduate School, 1998);Fleet Numerical Meteorology and Oceanography Center (FNMOC) forecasts the atmospheric environment and weather using several meteorological and oceanographic models. These models' forecasting abilities are verified by ...
Taylor, Ian (Monterey, California: Naval Postgraduate School, 2017-09);This research presents the first accurate three and six Degree of Freedom (DOF) models of the small diameter REMUS 100 with cross-tunnel thrusters (CTT). These are the first known hydrodynamic models to explicitly consider ...
An Experimental and Computational Investigation of Oscillating Airfoil Unsteady Aerodynamics at Large Mean Incidence Capece, Vincent R.; Platzer, Max F. (2003-03);A major challenge in the design and development of turbomachine airfoils for gas turbine engines is high cycle fatigue failures due to flutter and aerodynamically induced forced vibrations. In order to predict the aeroelastic ...