Title: Enterprise Modelling and Requirements Analysis using the i* Framework
Time: 14:00
Location: Meeting room, Ed. Zeta
Type: Research Result
Speaker: Talk by Novarun Deb
Abstract:We identify that the inherent sequence agnostic property of goal models prevents requirement analysts from performing compliance checks in the requirements phase itself as compliance rules are generally embedded with temporal information. This is where we propose the Semantic Implosion Algorithm that extracts a finite state model corresponding to a given goal model with the help of model transformation. This algorithm outperforms the existing solution by a factor of 1017, making our solution more efficient and scalable for deployment in the real world. We also develop the iToNuSMV tool that implements the Semantic Implosion Algorithm and performs model checking on i models. Subsequently, we go beyond structural analysis and try to explore the semantics associated with goal models and how they can be used in the goal model maintenance problem. Our final research contribution is the Annotation of Functional Semantics and their Reconciliation AFSR framework that provides a new goal model nomenclature that goes beyond the legacy nomenclature and associates semantics with individual goals. The framework also provides a reconciliation machinery that helps to perform semantic analysis and detect entailment or consistency conflicts within goal models. The framework also provides analysts with corrective measures that can be adopted to resolve such conflicts. We also demonstrate how the goal maintenance problem can be mapped to the state space search problem and an admissible and consistent heuristic path cost function allows us to deploy A search to find the optimal goal model configuration that is free from all conflicts.
Tag Archives: Model checking
29.05.2013 – Talk by Luca Bortolussi
Title: Mean field approximation for stochastic model checking
Time: 14:00
Location: Meeting room
Type: Research Result
Speaker: Luca Bortolussi
Abstract:
Mean field approximation techniques are well established approaches to analyse large-scale stochastic processes, especially population Markov models. Some years ago, they have entered the arena of quantitative formal methods, and they provided a consistent way to define fluid semantics for stochastic process algebras.
Here, we will discuss how mean field approximation can play a role in another successful area of quantitative formal methods, namely stochastic model checking. In particular, we will focus on a subclass of Continuous Stochastic Logic (CSL), considering formulae that expresses properties of single agents in a population model, and we will present an approximate model checking algorithm based on mean field approximation. We will also discuss model checking CSL formulae against time-inhomogeneous CTMC models, as this turns out to be the core procedure needed for fluid approximation.
Finally, we will consider a class of global properties that can be analysed by linear noise approximation, a higher order fluid approximation.
25.01.2013 – Talk by Hoang Vu Tuan
Title: The PRISM tool and its applications
Time: 14:00
Location: Meeting room
Type: Tool presentation
Speaker: Hoang Vu Tuan
Abstract:
In this presentation, I will consider some models and show how it is possible to derive some meaningful properties by using the PRISM model checker. PRISM tool supports four types of models whose underlying processes can be Discrete-time Markov chain (DTMC), Continuous-time
Markov chains (CTMC), Markov decision processes (MDP) and Probabilistic timed automata (PTA). For each of these classes, a set of properties can be analysed. The talk will rely on a case study to illustrate the PRISM functionalities. Specifically, the Stable Matching problem will be addressed by applying the DTMC analysis.
