Date: 23 October, 2008 (Wed)
Time: 10:00-12:00
Place: Seminar Room 1 (2006) on 20F, NII
Fee: Free
Contact: Kenji Taguchi (ktaguchi_AT_ nii.ac.jp)
−Towards Flexible and Efficient Fair System Verification
Jun Sun, School of Computing, National University of Singapore (NUS)
− Property Specifications for Workflow Modelling
Peter Wong, the Computing Laboratory, University of Oxford
Title: Towards Flexible and Efficient Fair System Verification
Speaker: Jun Sun, School of Computing, National University of Singapore (NUS)
Abstract:
Recent development on distributed systems has shown that a variety of fairness assumptions (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols.
Fairness is abstraction of a fair scheduler or the relative speed of processors. Current practice of system analysis is deficient under fairness. In this talk, I will introduce the toolkit (named PAT, available at http://www.comp.nus.edu.sg/~liuyang/pat)
developed for flexible and efficient system analysis under fairness assumptions. An improved model checking algorithm is designed to handle different fairness (e.g., weak fairness, strong local/global
fairness) flexibly. Partial order reduction which is effective for distributed system verification is extended to fair systems whenever possible. We show through theoretical arguments and empirical evaluation (on recent population protocols as well as benchmark
systems) that PAT outperforms current practice of verification under fairness. Previously unknown bugs have been revealed using PAT over systems functioning under strong global fairness.
Biography:
Dr. SUN, Jun received Bachelor of Science and PhD degree (on software
engineering) in School of Computing, National University of Singapore (NUS) in 2002 and 2006. Since 2006, he was named a Lee Kuan Yew Postdoctoral fellow at Department of Computer Science, NUS. His research interests are mainly in formal system specification, verification and synthesis. In particular, he has been working with a variety of different specification languages and notations in order to develop practical tools for elegant system development. More details about his research and background can be found at: http://www.comp.nus.edu.sg/~sunj
Title: Property Specifications for Workflow Modelling
Speaker: Peter Wong, the Computing Laboratory, University of Oxford
Abstract:
Previously we have provided two formal behavioural semantics for Business Process Modelling Notation (BPMN) in the process algebra CSP.
By exploiting CSP’s refinement orderings, developers may formally compare their BPMN models. However, BPMN is not a specification language, and it is difficult and sometimes impossible to construct behavioural properties against which BPMN models may be verified. In this talk we will present a pattern-based approach for capturing these behavioural properties. We will describe a property specification language PL for capturing a generalisation of Dwyer et al.’s Property Specification Patterns, and present a translation from PL into a bounded, positive fragment of linear temporal logic, which can then be automatically translated into CSP for simple refinement checking. We will demonstrate its application via a simple example. This is joint work with Jeremy Gibbons.
Biography:
Mr. Peter Wong is currently a research student at the Computing Laboratory, University of Oxford, supervised by Dr Jeremy Gibbons. His research area is in the use of formal techniques such as process algebras to reason about business process and workflow specifications.
Before joining Oxford, he completed his master degree by research at the University of Warwick, where he investigated energy consumption analyses at source code level. During 2004, he took up a research position at the Hong Kong Polytechnic University to investigate context-awareness in mobile computing.
