scientific article; zbMATH DE number 605917
From MaRDI portal
Publication:4301167
zbMath0855.68060MaRDI QIDQ4301167
Publication date: 13 July 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Refining privacy-aware data flow diagrams, Automatic generation of verified concurrent hardware using VHDL, Spatial and timing properties in highway traffic, Sound reasoning in \textit{tock}-CSP, On the semantics of unified modeling language diagrams using Z notation, Testing using CSP Models: Time, Inputs, and Outputs, An Event-B based approach for cloud composite services verification, No Need Knowing Numerous Neighbours, Circus Time with Reactive Designs, Behavioural Models for FMI Co-simulations, An Abstract Model for Proving Safety of Autonomous Urban Traffic, Verifying data refinements using a model checker, An analysis of refinement in an abortive paradigm, Efficient symbolic computation of process expressions, Semantics, calculi, and analysis for object-oriented specifications, Property transformation under specification change, \textsc{Conjure}: automatic generation of constraint models from problem specifications, Special issue: Perturbation methods and formal modeling for dynamic systems, Automated reasoning with restricted intensional sets, Incompleteness of relational simulations in the blocking paradigm, An observationally complete program logic for imperative higher-order functions, A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures, Designing a semantic model for a wide-spectrum language with concurrency, Unifying Theories of Programming in Isabelle, A Unary Semigroup Trace Algebra, Lazy Relations, Putting logic-based distributed systems on stable grounds, Composition mechanisms for retrenchment, Temporal-logic property preservation under Z refinement, Stepwise refinement of heap-manipulating code in Chalice, Unifying theories in ProofPower-Z, Categorical foundations for structured specifications in \(\mathsf{Z}\), Using formal reasoning on a model of tasks for FreeRTOS, Mechanised support for sound refinement tactics, Experiments in program verification using Event-B, Model evolution and refinement, Mechanical reasoning about families of UTP theories, JCML: A specification language for the runtime verification of Java card programs, Refinement-oriented models of Stateflow charts, A Stepwise Approach to Linking Theories, From control law diagrams to Ada via \textsf{Circus}, Safety-critical Java programs from \textsf{Circus} models, On the Purpose of Event-B Proof Obligations, A Practical Single Refinement Method for B, Domain science and engineering from computer science to the sciences of informatics. II: Science, Model checking RAISE applicative specifications, Domain science and engineering from computer science to the sciences of informatics. I: Engineering, Refinement modal logic, Data refinement and singleton failures refinement are not equivalent, Relational Concurrent Refinement: Automata, Test selection for traces refinement, Automating Event-B invariant proofs by rippling and proof patching, Completeness of ASM Refinement, More Relational Concurrent Refinement: Traces and Partial Relations, General Refinement, Part One: Interfaces, Determinism and Special Refinement, Modelling temporal behaviour in complex systems with Timebands, Manifest domains: analysis and description, Angelic processes for CSP via the UTP, On the purpose of Event-B proof obligations, A process algebraic framework for specification and validation of real-time systems, Completeness of fair ASM refinement, A tactic language for refinement of state-rich concurrent specifications, Formalisations and applications of BPMN, A Relative Timed Semantics for BPMN, Stateflow Diagrams in, Specification and Runtime Verification of Java Card Programs, Checking Z Data Refinements Using Traces Refinement, ASM refinement and generalizations of forward simulation in data refinement: a comparison, Abstract state machines: a unifying view of models of computation and of system design frameworks, Compositionality: Ontology and Mereology of Domains, Extended Static Checking by Calculation Using the Pointfree Transform, Modelling Divergence in Relational Concurrent Refinement, An abstract model for proving safety of autonomous urban traffic, Refinement and state machine abstraction, Type inference for set theory, Refinement and verification in component-based model-driven design, Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository, POSIX file store in Z/Eves: An experiment in the verified software repository, Test-data generation for control coverage by proof, On integrating confidentiality and functionality in a formal method, The behavioural semantics of Event-B refinement, 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, Towards Algebraic Semantics of Circus Time, A UTP semantics for \textsf{Circus}, Relational concurrent refinement. II: Internal operations and outputs, FDR explorer, Testing for refinement in \textsf{Circus}, Correct hardware synthesis, A formal framework for modeling and validating simulink diagrams, Simulink Timed Models for Program Verification, Proving Safety of Traffic Manoeuvres on Country Roads, A calculus for schemas in Z, Understanding, Explaining, and Deriving Refinement, Sound and Relaxed Behavioural Inheritance, Extended transitive separation logic, Type Checking Specifications, Generic Tools via General Refinement, Moded and continuous abstract state machines, Laws of mission-based programming
Uses Software
