Modeling in Event B. System and software engineering.
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Developing topology discovery in Event-B
- Modelling the embedded control system using iUML-B pattern state machine
- Event algebra for transition systems composition application to timed automata
- Relating trace refinement and linearizability
- A verification and deployment approach for elastic component-based applications
- Simulation relations for fault-tolerance
- Stepwise refinement of heap-manipulating code in Chalice
- External and internal choice with event groups in Event-B
- Security invariants in discrete transition systems
- IPL: an integration property language for multi-model cyber-physical systems
- Modelling resilient collaborative multi-agent systems
- Towards leveraging domain knowledge in state-based formal methods
- Moded and continuous abstract state machines
- Spot the difference: a detailed comparison between B and Event-B
- Flashix: modular verification of a concurrent and crash-safe flash file system
- Event-B refinement for continuous behaviours approximation
- Integrating formal specifications into applications: the ProB Java API
- Traits: correctness-by-construction for free
- Verifying autonomous systems
- Empowering the Event-B method using external theories
- Reachability analysis and simulation for hybridised Event-B models
- Operation caching and state compression for model checking of high-level models. How to have your cake and eat it
- Formal models for consent-based privacy
- Specification of systems with parameterised events: An institution-independent approach
- Test generation from event system abstractions to cover their states and transitions
- Bridging arrays and ADTs in recursive proofs
- Knowledge representation analysis of graph mining
- Semantics of Mizar as an Isabelle object logic
- On labeled birooted tree languages: algebras, automata and logic
- Specification and verification of concurrent programs through refinements
- Laws of mission-based programming
- Proof-based verification approaches for dynamic properties: application to the information system domain
- Theorem proving graph grammars with attributes and negative application conditions
- Combining refinement and signal-temporal logic for biological systems
- Possible values: exploring a concept for concurrency
- Monitorability for the Hennessy-Milner logic with recursion
- Consistency-preserving refactoring of refinement structures in Event-B models
- A formal framework for Hybrid Event B
- The refinement calculus of reactive systems
- scientific article; zbMATH DE number 1631956 (Why is no real title available?)
- Verification of \(\mathrm{EB}^3\) specifications using CADP
- Set-theoretic models of computations
- Pliant modalities in hybrid Event-B
- Practical theory extension in Event-B
- rCOS: defining meanings of component-based software architectures
- Proving Quicksort Correct in Event-B
- Specification of a localization component driven by a goal-based approach: some lessons we learned
- Association of under-approximation techniques for generating tests from models
- Concurrent abstract state machines
- Behavioural models for FMI co-simulations
- The subject-oriented approach to software design and the abstract state machines method
- Foundations for using linear temporal logic in Event-B refinement
- A proof-based method for modelling timed systems
- Checking the Conformance of a Promela Design to its Formal Specification in Event-B
- Incremental System Modelling in Event-B
- Experiments in program verification using Event-B
- Ambient abstract state machines with applications
- scientific article; zbMATH DE number 2080015 (Why is no real title available?)
- Putting logic-based distributed systems on stable grounds
- A behavioural theory of recursive algorithms
- scientific article; zbMATH DE number 7453194 (Why is no real title available?)
- Relational differential dynamic logic
- Building Specifications in the Event-B Institution
- Expressivity within second-order transitive-closure logic
- Refining autonomous agents with declarative beliefs and desires
- Refinement, decomposition, and instantiation of discrete models: application to Event-B
- Modeling numerical programs with Event-B
- Modelling Systems
- Linking event-B and concurrent object-oriented programs
- Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B
- Understanding, Explaining, and Deriving Refinement
- Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B
- Systematic Refinement of Abstract State Machines with Higher-Order Logic
- Refinement of Timing Constraints for Concurrent Tasks with Scheduling
- Verifiable Code Generation from Scheduled Event-B Models
- Information Flow Control-by-Construction for an Object-Oriented Language
- A formal model for blockchain-based consent management in data sharing
- Flexible Correct-by-Construction Programming
- Trace preservation in B and Event-B refinements
- Verification-Led Smart Contracts
- On the Introduction of Guarded Lists in Bach: Expressiveness, Correctness, and Efficiency Issues
- Efficient approximate verification of B and Z models via symmetry markers
- Simple feature engineering via neat default retrenchments
- Generating counterexamples for quantitative safety specifications in probabilistic B
- A modeling concept for formal verification of OS-based compositional software
- Linking formal methods in software development. A reflection on the development of rCOS
- Towards a model-checker for \textit{\textsf{Circus}}
- \textit{\textsf{Circus2CSP}}: a tool for model-checking \textit{\textsf{Circus}} using FDR
- Schematic program proofs with abstract execution. Theory and applications
- An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrency
- Extending rely-guarantee thinking to handle real-time scheduling
- Formal language semantics for triggered enable statecharts with a run-to-completion scheduling
- A deep reinforcement learning framework with formal verification
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- A complete fragment of LTL(EB)
- On the expressiveness and efficiency of guarded lists in Bach
- Automating Event-B invariant proofs by rippling and proof patching
- Refining constructive hybrid games
- Formal methods for mobile ad hoc networks: a survey
- Comparison of methods for modeling access control in OS and DBMS in Event-B for the purpose of their verification with Rodin and ProB tools
This page was built for publication: Modeling in Event B. System and software engineering.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3569584)
