ORCID Profile
0000-0003-4095-0732
Current Organisation
University of Southampton
Does something not look right? The information on this page has been harvested from data sources that may not be up to date. We continue to work with information providers to improve coverage and quality. To report an issue, use the Feedback Form.
Publisher: Springer International Publishing
Date: 11-11-2019
Publisher: Elsevier BV
Date: 12-2016
Publisher: Springer Nature Switzerland
Date: 2023
Publisher: IEEE
Date: 12-2018
Publisher: Elsevier BV
Date: 04-2021
Publisher: Springer International Publishing
Date: 2020
Publisher: Springer International Publishing
Date: 2020
Publisher: Springer International Publishing
Date: 2018
Publisher: Springer International Publishing
Date: 2018
Publisher: Springer International Publishing
Date: 2016
Publisher: Springer International Publishing
Date: 2021
Publisher: Elsevier BV
Date: 2023
Publisher: Springer International Publishing
Date: 2021
Publisher: Elsevier BV
Date: 2021
Publisher: Springer International Publishing
Date: 2017
Publisher: Springer International Publishing
Date: 11-11-2019
Publisher: Elsevier BV
Date: 06-2018
Publisher: Springer International Publishing
Date: 2023
Publisher: IEEE
Date: 06-2023
Publisher: Springer International Publishing
Date: 2019
Publisher: Springer Science and Business Media LLC
Date: 31-03-2020
Publisher: Association for Computing Machinery (ACM)
Date: 11-2016
DOI: 10.1007/S00165-016-0376-0
Abstract: In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.
Publisher: Springer International Publishing
Date: 2018
Publisher: Springer International Publishing
Date: 2017
Publisher: IEEE
Date: 11-2017
Publisher: Springer Science and Business Media LLC
Date: 04-03-2022
DOI: 10.1007/S11334-021-00416-4
Abstract: State chart notations with ‘run to completion’ semantics are popular with engineers for designing controllers that react to environment events with a sequence of state transitions but lack formal refinement and rigorous verification methods. State chart models are typically used to design complex control systems that respond to environmental triggers with a sequential process. The model is usually constructed at a concrete level and verified and validated using animation techniques relying on human judgement. Event-B, on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. Abstraction and formal verification provide greater assurance that critical (e.g. safety or security) properties are not violated by the control system. In this paper, we introduce a notion of refinement into a ‘run to completion’ state chart modelling notation and leverage Event-B’s tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into Event-B refinements and suggest a solution. We illustrate our approach and show how models can be validated at different refinement levels using our scenario checker animation tools. We show how critical invariant properties can be verified by proof despite the reactive nature of the system and how behavioural aspects of the system can be verified by testing the expected reactions using a temporal logic, model checking approach. To verify liveness, we outline a proof that the run to completion is deadlock-free and converges to complete the run.
Publisher: IEEE
Date: 10-2017
Publisher: Springer Science and Business Media LLC
Date: 25-01-2022
DOI: 10.1038/S41598-022-05308-6
Abstract: Constructing a large biological model is a difficult, error-prone process. Small errors in writing a part of the model cascade to the system level and their sources are difficult to trace back. In this paper we extend a recent approach based on Event-B, a state-based formal method with refinement as its central ingredient, allowing us to validate for model consistency step-by-step in an automated way. We demonstrate this approach on a model of the heat shock response in eukaryotes and its scalability on a model of the $$\\mathsf {ErbB}$$ ErbB signaling pathway. All consistency properties of the model were proved automatically with computer support.
Publisher: Springer Science and Business Media LLC
Date: 15-03-2015
Publisher: Sciendo
Date: 31-12-2020
Publisher: Springer Nature Switzerland
Date: 2022
Publisher: Springer International Publishing
Date: 2017
Publisher: Springer International Publishing
Date: 2023
Publisher: Springer International Publishing
Date: 2021
Location: United Kingdom of Great Britain and Northern Ireland
No related grants have been discovered for Thai Son Hoang.