ZiQian
Introduction:
Model checking, unlike other model-based analysis and development methods, is perhaps not as popular as it ought to be due to the fact that a good model is required beforehand. In the setting of PMC, users are further required to provide a probabilistic model with accurate distributions, which is often challenging. In practice, system modeling is often done manually, which is both time-consuming and error-prone. Worse, it could be infeasible if the system is a black box or it is simply too complicated so that no accurate model exists.
One way to avoid manual modeling is statistical model checking (SMC), which samples the system executions and apply hypothesis testing for verification purpose. Another approach we are more interested in is to automatically learn probabilistic models from system executions.
We investigate two categaries of learning algorithms: learn from multiple executions and learn from a single, long execution. The resulting models are both discrete-time Markov Chains (DTMCs). We propose a new learning framework based on evolution algorithms to provide better generalization from system executions compared to existing state-of-art algorithms, which orgnizes data as a tree and generalize a model based on it. We then conduct an empirical study on multiple case studies (see here) to compare the state-of-art learning algorithms, evolution-based algorithms and SMC in terms of effectiveness and efficiency. We also apply them on real-world complicated system (see water treatment system) where manual modeling is impossible.
Implementation:
The source code of the project is hosted in BitBucket. (Click here)
You can follow the project guideline to try out the case studies or format your own system executions to Ziqian input to run the learning algorithms.
Do try it out!
Key Publications
Automatically ‘Verifying’ Discrete-Time Complex Systems through Learning, Abstraction and Refinement.
IEEE Trans. Software Eng. 47(1).
Learning probabilistic models for model checking: an evolutionary approach and an empirical study.
Int. J. Softw. Tools Technol. Transf. 20(6).
People
