相关论文: A Formal Development Cycle for Security Engineerin…

Security-critical system requirements are increasingly enforced through mandatory access control systems. These systems are controlled by security policies, highly sensitive system components, which emphasizes the paramount importance of…

Privacy analysis is critical but also a time-consuming and tedious task. We present a formalization which eases designing and auditing high-level privacy properties of software architectures. It is incorporated into a larger policy analysis…

Computer systems process, store and transfer sensitive information which makes them a valuable asset. Despite the existence of standards such as ISO 27005 for managing information risk, cyber threats are increasing, exposing such systems to…

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 Engineering often adapts theory-building frameworks from the social sciences to address socio-technical complexity. The key phases of the theory-building process are conceptual development, operationalization, testing, and…

We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and…

Isabelle is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or `logical framework') in…

Automating experimental protocol design and execution remains as a fundamental bottleneck in realizing self-driving laboratories. We introduce PRISM (Protocol Refinement through Intelligent Simulation Modeling), a framework that automates…

In a traditional formal development process, e.g. using the B method, the informal user requirements are (manually) translated into a global abstract formal specification. This translation is especially difficult to achieve. The Event-B…

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…

Integrity of audit logs produced by Internet of Things (IoT) devices is a prerequisite for post-incident forensics, regulatory compliance, and operational accountability. While blockchain-backed logging infrastructures can satisfy this…

We provide simple equational principles for deriving rely-guarantee-style inference rules and refinement laws based on idempotent semirings. We link the algebraic layer with concrete models of programs based on languages and execution…

There is a lack of formalism for some key foundational concepts in systems engineering. One of the most recently acknowledged deficits is the inadequacy of systems engineering practices for engineering intelligent systems. In our previous…

In a recent paper, new theorems linking apparently unrelated mathematical objects (event structures from concurrency theory and full graphs arising in computational biology) were discovered by cross-site data mining on huge databases, and…

Sensor data in IoT (Internet of Things) systems is vulnerable to tampering or falsification when transmitted through untrusted services. This is critical because such data increasingly underpins real-world decisions in domains such as…

Having a clear view of events that occurred over time is a difficult objective to achieve in digital investigations (DI). Event reconstruction, which allows investigators to understand the timeline of a crime, is one of the most important…

Formal methods provide systematic and rigorous techniques for software development. We strongly believe that they must be taught in computer science curricula. In this paper we present the pedagogic rationale and the concrete implementation…

ICS environments are vital to the operation of critical infrastructure such as power grids, water treatment facilities, and manufacturing plants. However, these systems are vulnerable to cyber attacks due to their reliance on interconnected…

Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications,…

With ever-expanding computation and communication capabilities of modern embedded platforms, Internet of Things (IoT) technologies enable development of Reconfigurable Manufacturing Systems---a new generation of highly modularized…