An Application of Stochastic Model Checking in the Industry: User‐Centered Modeling and Analysis of Collaboration inThinkteam®
Maurice H. ter Beek, Stefania Gnesi, Diego Latella, Mieke Massink, Maurizio Sebastianis, Gianluca Trentanni · Formal Methods for Industrial Critical Systems · 2012
This chapter describes a general methodology for modeling and analyzing industrial software systems in their design phase, that is, prior to their implementation, by means of model checking. It uses qualitative and quantitative model checking to evaluate thinkteam, and three proposed extensions, to assist the design phase of this industrial collaborative system. The chapter illustrates the general methodology underlying all of the aforementioned experiences. It shows that model checking can be of great help in an exploratory design phase, both for comparing different design options and for refining and improving the description of the proposed extensions. This chapter starts with detailed descriptions of thinkteam and the log-file analysis. It describes the proposed thinkteam extension and its stochastic model, after which relevant correctness and performance properties are formalized and verified, and the outcome is interpreted. The chapter contains the lessons learned from this industrial case study and finally draws some conclusions. Controlled Vocabulary Terms product life cycle management; software engineering