scientific article
From MaRDI portal
Publication:3569584
zbMath1213.68214MaRDI QIDQ3569584
Publication date: 21 June 2010
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Theory of software (68N99)
Related Items
Theorem proving graph grammars with attributes and negative application conditions ⋮ 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 ⋮ Relational Differential Dynamic Logic ⋮ Combining refinement and signal-temporal logic for biological systems ⋮ Verification of \(\mathrm{EB}^3\) specifications using CADP ⋮ Sound verification procedures for temporal properties of infinite-state systems ⋮ Modelling the embedded control system using iUML-B pattern state machine ⋮ Possible values: exploring a concept for concurrency ⋮ Concurrent abstract state machines ⋮ A Proof-Based Method for Modelling Timed Systems ⋮ Behavioural Models for FMI Co-simulations ⋮ Building Specifications in the Event-B Institution ⋮ Event-B refinement for continuous behaviours approximation ⋮ Integrating formal specifications into applications: the ProB Java API ⋮ Checking the Conformance of a Promela Design to its Formal Specification in Event-B ⋮ Foundations for using linear temporal logic in Event-B refinement ⋮ Event algebra for transition systems composition application to timed automata ⋮ 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 ⋮ Monitorability for the Hennessy-Milner logic with recursion ⋮ The refinement calculus of reactive systems ⋮ rCOS: Defining Meanings of Component-Based Software Architectures ⋮ The Subject-Oriented Approach to Software Design and the Abstract State Machines Method ⋮ Consistency-preserving refactoring of refinement structures in Event-B models ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Relating trace refinement and linearizability ⋮ A verification and deployment approach for elastic component-based applications ⋮ Simulation relations for fault-tolerance ⋮ Putting logic-based distributed systems on stable grounds ⋮ Efficient approximate verification of B and Z models via symmetry markers ⋮ 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 ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ External and internal choice with event groups in Event-B ⋮ Security invariants in discrete transition systems ⋮ Verification-Led Smart Contracts ⋮ Integrating stochastic reasoning into Event-B development ⋮ On the Introduction of Guarded Lists in Bach: Expressiveness, Correctness, and Efficiency Issues ⋮ Experiments in program verification using Event-B ⋮ Ambient abstract state machines with applications ⋮ Unnamed Item ⋮ Simple feature engineering via neat default retrenchments ⋮ Test generation from event system abstractions to cover their states and transitions ⋮ Generating counterexamples for quantitative safety specifications in probabilistic B ⋮ Proving Quicksort Correct in Event-B ⋮ Specification of a Localization Component Driven by a Goal-Based Approach: Some Lessons We Learned ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Association of Under-Approximation Techniques for Generating Tests from Models ⋮ Refining autonomous agents with declarative beliefs and desires ⋮ Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B ⋮ Unnamed Item ⋮ IPL: an integration property language for multi-model cyber-physical systems ⋮ Modelling resilient collaborative multi-agent systems ⋮ Optimising the ProB model checker for B using partial order reduction ⋮ Refinement patterns for ASTDs ⋮ The behavioural semantics of Event-B refinement ⋮ Derivation of concurrent programs by stepwise scheduling of Event-B models ⋮ Introducing extra operations in refinement ⋮ Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application ⋮ Relational concurrent refinement. III: Traces, partial relations and automata ⋮ A formal framework for Hybrid Event B ⋮ Knowledge representation analysis of graph mining ⋮ A Behavioural Theory of Recursive Algorithms ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Set-Theoretic Models of Computations ⋮ Pliant Modalities in Hybrid Event-B ⋮ Practical Theory Extension in Event-B ⋮ Developing topology discovery in Event-B ⋮ Understanding, Explaining, and Deriving Refinement ⋮ On labeled birooted tree languages: algebras, automata and logic ⋮ Specification and verification of concurrent programs through refinements ⋮ Towards leveraging domain knowledge in state-based formal methods ⋮ Moded and continuous abstract state machines ⋮ Laws of mission-based programming ⋮ Proof-based verification approaches for dynamic properties: application to the information system domain ⋮ Spot the difference: a detailed comparison between B and Event-B ⋮ Flashix: modular verification of a concurrent and crash-safe flash file system
Uses Software
