Verification and Validation of Behavior Models Using Lightweight Formal Methods

The article of record as published may be found at http://dx.doi.org/10.1007/978-3-319-62217-0_31The 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.Consortium for Robotics and Unmanned Systems Education and Research (CRUSER)Best Transition in Systems Engineering Research, Conference on Systems Engineering Research, March 23, 201