Exploring the twin peaks using probabilistic verification techniques

Anitha Murugesan, Sanjai Rayadurgam, Lu Feng, Michael W. Whalen, Mats P E Heimdahl, Insup Lee

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

System requirements and system architecture/design co-evolve as the understanding of both the problem at hand as well as the solution to be deployed evolve-the Twin Peaks concept. Modeling of requirements and solution is a promising approach for exploring the Twin Peaks. Commonly, such models are deterministic because of the choice of modeling notation and available analysis tools. Unfortunately, most systems operate in an uncertain environment and contain physical components whose behaviors are stochastic. Although much can be learned from modeling and analysis with commonly used tools, e.g., Simulink/Stateow and the Simulink Design Verifier, the SCADE toolset, etc., the results from the exploration of the Twin Peaks will-by necessity-be inaccurate and can be misleading; inclusion of the probabilistic behavior of the physical world provides crucial additional insight into the system's required behavior, its operational environment, and the solution proposed for its software. Here, we share our initial experiences with model-based deterministic and probabilistic verification approaches while exploring the Twin Peaks. The intent of this paper is to demonstrate how probabilistic reasoning helps illuminate weaknesses in system requirements, environmental assumptions, and the intended software solution, that could not be identified when using deterministic techniques. We illustrate our experience through a medical device sub-system, modeled and analyzed using the Simulink/Stateow (deterministic) and PRISM (probabilistic) tools.

Original languageEnglish (US)
Title of host publication4th International Workshop on the Twin Peaks of Requirements and Architecture, TwinPeaks 2014 - Proceedings
PublisherAssociation for Computing Machinery, Inc
Pages18-23
Number of pages6
ISBN (Electronic)9781450328487
DOIs
StatePublished - Jun 1 2014
Event4th International Workshop on the Twin Peaks of Requirements and Architecture, TwinPeaks 2014 - Hyderabad, India
Duration: Jun 1 2014 → …

Publication series

Name4th International Workshop on the Twin Peaks of Requirements and Architecture, TwinPeaks 2014 - Proceedings

Other

Other4th International Workshop on the Twin Peaks of Requirements and Architecture, TwinPeaks 2014
CountryIndia
CityHyderabad
Period6/1/14 → …

Keywords

  • Architecture
  • Model based verification
  • Requirements

Fingerprint Dive into the research topics of 'Exploring the twin peaks using probabilistic verification techniques'. Together they form a unique fingerprint.

Cite this