Developed in Isabelle/HOL 2019
PiCore is an event-based and parametric rely-guarantee framework for concurrent reactive systems (e.g., concurrent OS kernels, control systems, communication systems). We introduce ``events'' and their compositions into the rely-guarantee method for system reactions. Our approach supports compositional verification of functional correctness and safety as well as deals with concurrency in systems (e.g. multicore concurrency and interruptible concurrency). PiCore decouples the rely-guarantee reasoning of programs from that of the events by a clear rely-guarantee interface. It is thus able to integrate existing imperative languages for programs and their rely-guarantee proof systems.
Browse the Isabelle/HOL sources of PiCore
CSimpl is a generic and realistic imperative language by extending the Simpl language and providing a rely-guarantee proof system in Isabelle/HOL. Simpl is able to represent a large subset of C99 code supported by a translation tool C-to-Isabelle parser. Simpl and its verification framework with a Floyd/Hoare-like logic have been applied to the formal verification of seL4 OS kernel at C code level.
We have integrated the CSimpl language and its rely-guarantee proof system into PiCore without changing any source code of CSimpl.
Browse the Isabelle/HOL sources of CSimpl
Browse the Isabelle/HOL sources of PiCore_CSimpl
SIMP is a simple imperative language with a rely-guarantee proof system in Isabelle/HOL as the HOL-Hoare_Parallel lib (under the directory of Isabelle2018/src/HOL/Hoare_Parallel).
We have integrated the SIMP language and its rely-guarantee proof system into PiCore without changing any source code of HOL-Hoare_Parallel. We extend SIMP by some new rely-guarantee proof rules. Two examples, an stepper motor and an ARINC 653 OS, are created using PiCore_SIMP.
Browse the Isabelle/HOL sources of SIMP
Browse the Isabelle/HOL sources of PiCore_SIMP
We use the PiCore to formally specify and verify the concurrent memory management of Zephyr RTOS. The C code is ~ 400 lines, not counting blank lines and comments. We develop a fine-grained low level formal specification of buddy memory management. The specification has a basically line-to-line correspondence with the Zephyr C code, covering all the data structures and imperative statements present in the implementation. During the formal verification, we found 3 bugs in the C code of Zephyr which are: an incorrect block split, an incorrect return, and non-termination of a loop in the k_mem_pool_alloc service.
Browse the Isabelle/HOL sources of Zephyr
BPEL aims to model the behavior of processes via a language for the specification of both executable and abstract business processes. It extends the Web Services interaction model and enables it to support business transactions. BPEL has complex basic and structural activities, such asreceive, reply, invoke, sequence, while, repeatuntil, flow (parallel). We have applied PiCore to interpret the semantics of the BPEL language by translating BPEL into PiCore. To show the correctness of this translation, we prove a strong bisimulation between the source BPEL program and the translated PiCore specification. In this way, formal verification of BPEL programs can be conducted in the PiCore framework. The strong bisimulation implies the soundness and completeness of formal verification of BPEL program in PiCore.