相关论文: Dependability Engineering in Isabelle

We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the…

Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development…

Confidentiality, integrity, availability, authenticity, authorization, and accountability are known as security properties that secure systems should preserve. They are usually considered as security final goals that are achieved by system…

Assurance cases are often required as a means to certify a critical system. Use of formal methods in assurance can improve automation, and overcome problems with ambiguity, faulty reasoning, and inadequate evidentiary support. However,…

To develop trustworthy distributed systems, verification techniques and formal methods, including lightweight and practical approaches, have been employed to certify the design or implementation of security protocols. Lightweight formal…

Autonomous systems must sustain justified confidence in their correctness and safety across their operational lifecycle-from design and deployment through post-deployment evolution. Traditional assurance methods often separate…

This set of theories presents a formalisation in Isabelle/HOL+Isar of data dependencies between components. The approach allows to analyse system structure oriented towards efficient checking of system: it aims at elaborating for a concrete…

The severity of recent vulnerabilities discovered on modern CPUs, e.g., Spectre [1], highlights how information leakage can have devas-tating effects to the security of computer systems. At the same time, it suggests that confidentiality…

As smart contracts are growing in size and complexity, it becomes harder and harder to ensure their correctness and security. Due to the lack of isolation mechanisms a single mistake or vulnerability in the code can bring the whole system…

LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's…

We propose inheritance and refinement relations for a CSP-based component model (BRIC), which supports a constructive design based on composition rules that preserve classical concurrency properties such as deadlock freedom. The proposed…

Event-B is a formal approach oriented to system modeling and analysis. It supports refinement mechanism that enables stepwise modeling and verification of a system. By using refinement, the complexity of verification can be spread and…

Refinement in Event-B supports the development of systems via proof based step-wise refinement of events. This refinement approach ensures safety properties are preserved, but additional reasoning is required in order to establish liveness…

Software developed using modern agile practices delivers a stream of software versions that require continuous regression testing rather than testing once close to the delivery or maintenance phase, as assumed by classical…

Formally verifying properties of software code has been a highly desirable task, especially with the emergence of LLM-generated code. In the same vein, they provide an interesting avenue for the exploration of formal verification and…

Interactive theorem provers are complex systems that require sophisticated platform efforts - and hence systems programming environments - to manage effectively. The Isabelle platform exemplifies this with its Isabelle/Scala systems…

This paper presents a formalisation of pGCL in Isabelle/HOL. Using a shallow embedding, we demonstrate close integration with existing automation support. We demonstrate the facility with which the model can be extended to incorporate…

A protocol-independent secrecy theorem is established and applied to several non-trivial protocols. In particular, it is applied to protocols proposed for protecting the computation results of free-roaming mobile agents doing comparison…

The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem-provers, thus providing a…

In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a secure information flow by checking a program after…