System Analysis and Verification Group

Our group has had a paper accepted at the 14th International Conference on Quantitative Evaluation of SysTems (QEST 2017) about our work on statistical model checking. An extended PDF version is available online now:

• C. Jegourel, J. Sun, and J. S. Dong. Sequential schemes for frequentist estimation of properties in statistical model checking. In Proc. International Conference on Quantitative Evaluation of SysTems (QEST 2017), LNCS, Springer, 2017.
  [Bibtex]

  @inproceedings{Jegourel-Sun-Dong17a,
  author = {Cyrille Jegourel and Jun Sun and Jin Song Dong},
  title = {Sequential Schemes for Frequentist Estimation of Properties in Statistical Model Checking},
  booktitle = {{Proc. International Conference on Quantitative Evaluation of SysTems (QEST 2017)}},
  year = {2017},
  series = {LNCS},
  publisher = {Springer},
  note = {To appear},
  pdf = {https://sav.sutd.edu.sg/wp-content/uploads/2016/08/QEST17_extended_version.pdf},
  }

Statistical Model Checking (SMC) is an approximate verification method that overcomes the state space explosion problem for probabilistic systems by Monte Carlo simulations. Simulations might be however costly if many samples are required. It is thus necessary to implement efficient algorithms to reduce the sample size while preserving precision and accuracy. In the literature, some sequential schemes have been provided for the estimation of property occurrence based on predefined confidence and absolute or relative error. Nevertheless, these algorithms remain conservative and may result in huge sample sizes if the required precision standards are demanding. In this article, we compare some useful bounds and some sequential methods based on frequentist estimations. We propose outperforming and rigorous alternative schemes, based on Massart bounds and robust confidence intervals. Our theoretical and empirical analysis show that our proposal reduces the sample size while providing guarantees on error bounds.

Our group has had a paper accepted at the 29th International Conference on Computer Aided Verification (CAV 2017) about our work on decidable fragments of separation logic. A PDF postprint is available online now:

• Q. L. Le, T. Makoto, J. Sun, and W. Chin. A decidable fragment in separation logic with inductive predicates and arithmetic. In Proc. International Conference on Computer Aided Verification (CAV 2017), LNCS, Springer, 2017.
  [Bibtex]

  @inproceedings{Le-Makoto-Sun-Chin17a,
  author = {Quang Loc Le and Tatsuta Makoto and Jun Sun and Wei-Ngan Chin},
  title = {A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic},
  booktitle = {{Proc. International Conference on Computer Aided Verification (CAV 2017)}},
  year = {2017},
  series = {LNCS},
  publisher = {Springer},
  note = {To appear},
  pdf = {https://sav.sutd.edu.sg/wp-content/uploads/2016/08/cav2017.pdf},
  }

We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets. Our decision procedure is based on a novel algorithm to infer a finite representation for each inductive predicate which precisely characterises its satisfiability. Our analysis shows that the proposed algorithm runs in exponential time in the worst case. We have implemented our decision procedure and integrated it into an existing verification system. Our experiment on benchmarks shows that our procedure helps to verify the benchmarks effectively.

Our group has published a new article at the 20th International Conference on Fundamental Approaches to Software Engineering (FASE 2017) about our work on learning probabilistic models for model checking:

• J. Wang, J. Sun, Q. Yuan, and J. Pang. Should we learn probabilistic models for model checking? A new approach and an empirical study. In Proc. International Conference on Fundamental Approaches to Software Engineering (FASE 2017), volume 10202, LNCS, Springer, 2017, pp. 3-21.
  [Bibtex]

  @inproceedings{Wang-Sun-Yuan-Pang17a,
  author = {Jingyi Wang and
  Jun Sun and
  Qixia Yuan and
  Jun Pang},
  title = {Should We Learn Probabilistic Models for Model Checking? {A} New Approach and An Empirical Study},
  booktitle = {{Proc. International Conference on Fundamental Approaches to Software Engineering (FASE 2017)}},
  series = {LNCS},
  volume = {10202},
  publisher = {Springer},
  pages = {3--21},
  year = {2017},
  doi = {10.1007/978-3-662-54494-5_1},
  pdf = {http://arxiv.org/abs/1605.08278},
  }

Many automated system analysis techniques (e.g., model checking, model-based testing) rely on first obtaining a model of the system under analysis. System modeling is often done manually, which is often considered as a hindrance to adopt model-based system analysis and development techniques. To overcome this problem, researchers have proposed to automatically “learn” models based on sample system executions and shown that the learned models can be useful sometimes. There are however many questions to be answered. For instance, how much shall we generalize from the observed samples and how fast would learning converge? Or, would the analysis result based on the learned model be more accurate than the estimation we could have obtained by sampling many system executions within the same amount of time? In this work, we investigate existing algorithms for learning probabilistic models for model checking, propose an evolution-based approach for better controlling the degree of generalization and conduct an empirical study in order to answer the questions. One of our findings is that the effectiveness of learning may sometimes be limited.

Two full papers co-authored by our group members were recently accepted to the 18th International Conference on Formal Engineering Methods (ICFEM 2016), which will be held in Tokyo, Japan later this month.

Postprints and DOI links for the papers are available below. The first paper proposes a framework to dynamically monitor and adapt the workflow of web service composition in order to automatically satisfy non-functional requirements. The second paper proposes a BDD-based verification technique for real-time systems.

• M. Chen, T. H. Tan, J. Sun, J. Wang, Y. Liu, J. Sun, and J. S. Dong. Service adaptation with probabilistic partial models. In Proc. International Conference on Formal Engineering Methods (ICFEM 2016), volume 10009, LNCS, Springer, 2016, pp. 122-140.
  [Bibtex]

  @inproceedings{Chen_et-al16a,
  author = {Manman Chen and
  Tian Huat Tan and
  Jun Sun and
  Jingyi Wang and
  Yang Liu and
  Jing Sun and
  Jin Song Dong},
  title = {Service Adaptation with Probabilistic Partial Models},
  booktitle = {{Proc. International Conference on Formal Engineering Methods (ICFEM 2016)}},
  pages = {122--140},
  series = {LNCS},
  volume = {10009},
  publisher  = {Springer},
  year = {2016},
  doi = {10.1007/978-3-319-47846-3_9},
  pdf = {https://sav.sutd.edu.sg/wp-content/uploads/2016/08/icfem2016-jingyi.pdf},
  }

• T. K. Nguyen, T. H. Tan, J. Sun, J. Li, Y. Liu, M. Chen, and J. S. Dong. Scaling BDD-based timed verification with simulation reduction. In Proc. International Conference on Formal Engineering Methods (ICFEM 2016), volume 10009, LNCS, Springer, 2016, pp. 363-382.
  [Bibtex]

  @inproceedings{Nguyen_et-al16a,
  author  = {Truong Khanh Nguyen and Tian Huat Tan and Jun Sun and Jiaying Li and Yang Liu and Manman Chen and Jin Song Dong},
  title = {Scaling {BDD}-based Timed Verification with Simulation Reduction},
  booktitle  = {{Proc. International Conference on Formal Engineering Methods (ICFEM 2016)}},
  pages = {363--382},
  volume = {10009},
  series = {LNCS},
  publisher = {Springer},
  year = {2016},
  doi = {10.1007/978-3-319-47846-3_23},
  pdf = {https://sav.sutd.edu.sg/wp-content/uploads/2016/08/icfem2016-jiaying.pdf},
  }

Two full papers and a short paper co-authored by our group members were recently accepted by the 21st International Symposium on Formal Methods (FM 2016), which will be held in Limassol, Cyprus this November.

Postprints of the papers are available below. The first paper resulted from our work on verifying time-based security protocols, whereas the latter two resulted from our work on analysing and verifying real-world cyber-physical systems such as the SWaT Secure Water Treatment testbed at SUTD.

• L. Li, J. Sun, and J. S. Dong. Automated verification of timed security protocols with clock drift. In Proc. International Symposium on Formal Methods (FM 2016), LNCS-FM, Springer, 2016.
  [Bibtex]

  @inproceedings{Li-Sun-Dong16a,
  author = {Li Li and Jun Sun and Jin Song Dong},
  title = {Automated Verification of Timed Security Protocols with Clock Drift},
  booktitle = {{Proc. International Symposium on Formal Methods (FM 2016)}},
  series = {LNCS-FM},
  publisher = {Springer},
  year = {2016},
  pdf = {https://sav.sutd.edu.sg/wp-content/uploads/2016/08/Li-Sun-Dong.FM_.2016.pdf},
  note = {To appear},
  }

• P. Kong, Y. Li, X. Chen, J. Sun, M. Sun, and J. Wang. Towards concolic testing for hybrid systems. In Proc. International Symposium on Formal Methods (FM 2016), LNCS-FM, Springer, 2016.
  [Bibtex]

  @inproceedings{Kong-et_al16a,
  author = {Pingfan Kong and Yi Li and Xiaohong Chen and Jun Sun and Meng Sun and Jingyi Wang},
  title = {Towards Concolic Testing for Hybrid Systems},
  booktitle = {{Proc. International Symposium on Formal Methods (FM 2016)}},
  series = {LNCS-FM},
  publisher = {Springer},
  year = {2016},
  pdf = {https://sav.sutd.edu.sg/wp-content/uploads/2016/08/HyChecker-FM2016.pdf},
  note = {To appear},
  }

• Y. Chen, C. M. Poskitt, and J. Sun. Towards learning and verifying invariants of cyber-physical systems by code mutation. In Proc. International Symposium on Formal Methods (FM 2016), LNCS-FM, Springer, 2016.
  [Bibtex]

  @inproceedings{Chen-Poskitt-Sun16a,
  author = {Yuqi Chen and Christopher M. Poskitt and Jun Sun},
  title = {Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation},
  booktitle = {{Proc. International Symposium on Formal Methods (FM 2016)}},
  series = {LNCS-FM},
  publisher = {Springer},
  year = {2016},
  pdf = {https://sav.sutd.edu.sg/wp-content/uploads/2016/08/Chen-Poskitt-Sun.FM_.2016.pdf},
  note = {To appear},
  }