Verification and Validation of Behavior Models Using Lightweight Formal Methods

Loading...
Thumbnail Image
Authors
Giammarco, Kristin
Giles, Kathleen
Subjects
Verification
Behavior modeling
System of systems
Formal methods
Monterey Phoenix
Validation
Advisors
Date of Issue
2018
Date
Publisher
Springer
Language
Abstract
The research described herein provides a method for exposing invalid behaviors in systems of systems (SoS) early in design, at the architecture level. The Monterey Phoenix (MP)-based method for conducting behavior model verification and validation (V&V) was developed after students ranging from high school to the graduate level began discovering unintended, invalid, and potentially high consequence behaviors permitted by their designs. These unspecified behaviors were consistent with known requirements, but violated stakeholder intent. Examples from four models from different domains and developed by different students are presented, then used as a basis for developing a structured set of behavior model V&V criteria that may be applied to any MP model. Finally, the criteria are put into the context of a systematic method that guides modelers in a thorough V&V of the behavior model. The ease with which unspecified and potentially invalid behaviors were exposed by students at various levels of education suggests that this lightweight formal method approach for behavior model V&V is user-friendly for application by practitioners who have basic skills in logic and logical thinking. Follow-on work will further test the method on other MP behavior modeling efforts, with an aim to improve and extend behavior model V&V criteria and the methods in which they are employed.
Type
Book Chapter
Description
The article of record as published may be found at http://dx.doi.org/10.1007/978-3-319-62217-0_31
Series/Report No
Department
Systems Engineering (SE)
Organization
Naval Postgraduate School (U.S.)
Identifiers
NPS Report Number
Sponsors
Consortium for Robotics and Unmanned Systems Education and Research (CRUSER)
Funder
Format
17 p.
Citation
Giammarco, K. and Giles, K., 2018. Verification and validation of behavior models using lightweight formal methods. In Disciplinary Convergence in Systems Engineering Research (pp. 431-447). Springer, Cham.
Distribution Statement
Rights
This 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.
Collections