A5042805366- Formal Methods in Verification
- Logic, programming, and type systems
- Model-Driven Software Engineering Techniques
- Software Reliability and Analysis Research
- Advanced Software Engineering Methodologies
- Distributed systems and fault tolerance
- Safety Systems Engineering in Autonomy
- Software Testing and Debugging Techniques
- Security and Verification in Computing
- Business Process Modeling and Analysis
- Systems Engineering Methodologies and Applications
- Parallel Computing and Optimization Techniques
- Scientific Computing and Data Management
- Logic, Reasoning, and Knowledge
- Simulation Techniques and Applications
- Semantic Web and Ontologies
- Service-Oriented Architecture and Web Services
- Real-Time Systems Scheduling
- Advanced Malware Detection Techniques
- Transportation Systems and Safety
- Gene Regulatory Network Analysis
- Adversarial Robustness in Machine Learning
- Microbial Metabolic Engineering and Bioproduction
- Advanced Data Processing Techniques
- Advanced Database Systems and Queries
University of Southampton
2016-2024
VinUniversity
2021
ETH Zurich
2008-2015
Hitachi (Japan)
2015
École Polytechnique Fédérale de Lausanne
2011
UNSW Sydney
2003-2006
Abstract Two methods have been identified for Event‐B model decomposition: shared variable and event. The purpose of this paper is to introduce the two approaches respective tool support in Rodin platform. Besides alleviating complexity large systems proofs, decomposition allows team development parallel over same project which very attractive industrial environment. Copyright © 2011 John Wiley & Sons, Ltd.
Abstract Safety and security are key considerations in the design of critical systems. Requirements analysis methods rely on expertise experience human intervention to make judgements. While judgement is essential an method, it also important ensure a degree formality so that we reason about safety at early stages design, rather than detect problems later. In this paper, present hierarchical incremental process aims justify flow-down derived requirements arising from hazards vulnerabilities...
Event-B developments are mostly structured around the refinement relationship. This top-down development architecture enables system details to be gradually introduced into formal model. However, this results in large models with monolithic structures. We develop a composition mechanism allowing bottom-up. In particular, our proposed works seamlessly existing technique Event-B. As result we have built method that can take advantage of both and bottom-up approaches. prove correctness machine...
Event-B has given developers the opportunity to construct models of complex systems which are correct by construction. However, there is no systematic approach, especially in terms reusing, could help with construction these models. We introduce notion design patterns within framework shorten this gap. Our approach preserves correctness critical formal methods and also reduces proving effort. Within our an pattern just another model devoted formalisation a typical sub-problem. As result, we...
Model decomposition is a powerful tool to scale the design of large and complex systems. It enables developers separate components development from concerns their integration orchestration. Event-B refinementbased formal method, equipped with three styles that come solid semantic foundations strong support. This paper intends give some useful insights modelling guidelines for using these styles, illustrated by an actual master data updating system.
Abstract In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. particular, the results presented in allow properties to be established for abstract system models, and identify conditions ensure that (suitably translated) continue hold as those models are developed through refinement. There several novel elements achievement: (1) LTL mapped across chains; (2) provide translations predicates reflect introduction events renaming...
We introduce a high-quality and large-scale Vietnamese-English parallel dataset of 3.02M sentence pairs, which is 2.9M pairs larger than the benchmark machine translation corpus IWSLT15. conduct experiments comparing strong neural baselines well-known automatic engines on our find that in both human evaluations: best performance obtained by fine-tuning pre-trained sequence-to-sequence denoising auto-encoder mBART. To knowledge, this first study. hope publicly available study can serve as...