A5057475070- Formal Methods in Verification
- Logic, programming, and type systems
- Software Testing and Debugging Techniques
- Model-Driven Software Engineering Techniques
- Distributed systems and fault tolerance
- Software Reliability and Analysis Research
- Simulation Techniques and Applications
- Advanced Database Systems and Queries
- Nuclear Issues and Defense
- Nuclear physics research studies
- Logic, Reasoning, and Knowledge
- Nuclear reactor physics and engineering
- Cryptographic Implementations and Security
- Diverse Scientific and Engineering Research
- Social Policies and Family
- Real-Time Systems Scheduling
- European and International Law Studies
- Semantic Web and Ontologies
- Embedded Systems Design Techniques
- Advanced Malware Detection Techniques
- Risk and Safety Analysis
- Business Process Modeling and Analysis
- Safety Systems Engineering in Autonomy
- Security and Verification in Computing
- Intelligent Tutoring Systems and Adaptive Learning
Centre Paul Albert-Février
2010-2020
ETH Zurich
2006
Abstract Event‐B is a formal notation and method for the systems development. The key feature of this to produce correct‐by‐construction system designs. Once correct design established, remaining work generate or implement code from design. Two main problems remain in process software. First, “quasi‐correct” due some technical limitations. For instance, it still difficult prove liveness properties by Rodin platform; not possible construct with floating‐point arithmetic, sometimes, model...
This work addresses the correct translation of an Event-B model to C code via intermediate formal language, HLL. The proof correctness follows two main steps. First, final refinement model, including invariants, is translated At that point, additional properties (e.g., deadlock-freeness, liveness properties, etc.) are added HLL model. invariants and at level guarantees translation. Second, automatically generated from for most system functions manually remaining ones; in this case, provides...
The Theory plug-in enables modellers to extend the mathematical modelling notation for Event-B, with accompanying support reasoning about extended language. Previous version of has been implemented based on Rodin 2.x. This presentation outline main improvements The- ory plug-in, be compatible 3.x, in terms both reliability and us- ability. We will also present changes that were needed core accommodate plug-in. Finally, we identify future enhancements research directions
Cet article presente quelques resultats du projet RNTL BOM (B Optimisant la Memoire). Le but etait d'obtenir un traducteur langage B vers le C, facilement adaptable a des contraintes memoire (logiciels embarques sur cartes puce). Nous proposons une methode d'extension types de base permettant d'inclure certains cible. presentons comment est decrit sous forme regles traduction pour permettre d'adapter aux plates-formes cibles. indiquons demarche assurer correction code produit. terminons par...