System Behavior Specification Verification and Validation (V&V)

Abstract

This chapter provides practitioners with an approach to verify and validate existing system behavior specifications using the Monterey Phoenix (MP) language, approach, and tool. First, a behavior specification is obtained in its native language, such as systems modeling language (SysML). If the mission, system behavior, or process that modeled is lengthy, it is partitioned into separate specifications for each phase. Each specification is then transcribed into an MP model and elaborated with potential alternative event flows. Next, each model is probed for emergent behaviors by running it through the MP event trace generator to produce the scope-complete set possible execution traces. The user inspects the traces for the presence of expected behaviors (supporting verification) and scans for the presence of potential unexpected yet plausible behaviors (supporting validation), documenting the findings. The findings are then used to update the original behavior specification, which may include the imposition of previously undocumented requirements, constraints, or assumptions that are newly realized. For a practitioner concerned about as-yet unknown, unexpected, and unwanted behaviors, a scope-complete set of MP execution traces generated from their specification represents a substantial data source that can be mined for the discovery of previously unrealized event flows that could arise as “extra” behaviors in the absence of any constraint to control them.

Leads

Kristin Giammarco

Naval Postgraduate School

Publications

Auguston, M. (2009a). Software architecture built from behavior models. ACM SIGSOFT Software Engineering Notes 34 (5): 1–15.
Auguston, M. (2009b). Monterey phoenix, or how to make software architecture executable. In: Proceedings of the 24th ACM SIGPLAN Conference Companion on Object Oriented Programming Systems Languages and Applications, Orlando, FL (25–29 October 2009), 1031–1040. ACM.
Auguston, M. (2020). System and software architecture and workflow modeling language manual. https://wiki.nps.edu/display/MP/Documentation (accessed 6 June 2023).
Auguston, M., Kristin Giammarco, W., Baldwin, C., and Farah-Stapleton, M. (2015). Modeling and verifying business processes with Monterey Phoenix. Procedia Computer Science 44: 345–353.
Berry, D. (1999). Formal methods: the very idea, some thoughts about why they work when they work. In: Proceedings of the 1998 ARO/ONR/NSF/ARPA Monterey Workshop on Engineering Automation for Computer Based Systems, Electronic Notes in Theoretical Computer Science, Monterey, CA, vol. 25, 10–22. https://doi.org/10.1016/S1571-0661(04)00127-6.
Blackburn, M., Peak, R., Baker, A., et al. (2019). Transforming Systems Engineering Through Model-Centric Engineering. Final Technical Report SERC-2019-TR-005. Systems Engineering Research Center: Hoboken, NJ, USA.
Borshchev, A. and Filippov, A.. (2004). From system dynamics and discrete event to practical agent based modeling: reasons, techniques, tools. In Proceedings of the 22nd International Conference of the System Dynamics Society, Oxford, England (25–29 July 2004) (Vol. 22). System Dynamics Society.
Easterbrook, S., Robin Lutz, R., Covington, J. et al. (1998). Experiences using lightweight formal methods for requirements modeling. IEEE Transactions on Software Engineering 24 (1): 4–14.
Giammarco, K. (2022). Exposing and controlling emergent behaviors using models with human reasoning. In: Emergent Behavior in System of Systems Engineering (ed. L.B. Rainey and O.T. Holland), 23–61. CRC Press.
Giammarco, K. and Giles, K. (2017). Verification and validation of behavior models using lightweight formal methods. In: Proceedings of the 15th Annual Conference on Systems Engineering Research, Redondo Beach, CA (23–25 March 2017). Procedia Computer Science.
Giammarco, K. and Shifflett, D. (2018a). Small package delivery baseline case. https://gitlab.nps.edu/monterey-phoenix/mp-model-collection/preloaded-examples/-/blob/master/models/Application_examples/Small_Package_Delivery_Basline_Case.mp (accessed 6 June 2023).
Giammarco, K. and Shifflett, D. (2018b). Small package delivery creative expansion. https://gitlab.nps.edu/monterey-phoenix/mp-model-collection/preloaded-examples/-/blob/master/models/Application_examples/Small_Package_Delivery_Creative_Expansion.mp
Giammarco, K. and Shifflett, D. (2018c). Small package delivery emergent behavior. https://gitlab.nps.edu/monterey-phoenix/mp-model-collection/preloaded-examples/-/blob/master/models/Application_examples/Small_Package_Delivery_Emergent_Behavior.mp
Giammarco, Kristin; Ron Carlson, Mark Blackburn, et al. (2018). Verification and Validation (V&V) of System Behavior Specifications. Final Technical Report SERC-2018-TR-116. Systems Engineering Research Center: Hoboken, NJ, USA.
Hall, J., Le, K., Patel, K., and Savacool, M. (2022). Assessing interoperability between behavior diagrams constructed with system modeling language (SysML) and Monterey Phoenix (MP). Master’s capstone report. Naval Postgraduate School.
Jackson, D. (2012). Software Abstractions: Logic, Language, and Analysis (Revised edition). MIT Press.
Ruppel, S.R. (2016). System behavior models: a survey of approaches. Master’s thesis. Naval Postgraduate School.
SEBoK Authors (2022a). System verification. in BKCASE Editorial Board. Guide to the Systems Engineering Body of Knowledge (SEBoK), v. 2.6 released 20 May, 2022. https://www.sebokwiki.org/wiki/System_Verification (accessed 21 February2023).
SEBoK Authors (2022b). System validation. in BKCASE Editorial Board. Guide to the Systems Engineering Body of Knowledge (SEBoK), v. 2.6 released 20 May, 2022. https://www.sebokwiki.org/wiki/System_Validation
Woodcock, J., Larsen, P.G., Bicarregui, J., and Fitzgerald, J. (2009). Formal methods: Practice and experience. ACM Computing Surveys (CSUR) 41 (4): 19.