A Survey on Formal Specification and Verification of Smart Mass Transit Railway Interlocking System

Nowadays interest in Smart Mass Transit Rail has grown-up to a large extent in a metropolitan area as the need for urban mobility has increased steadily. The reliability of software being used in such mass transit rail is crucial for us, specifically when software crashes may lead to catastrophic loss of human life and assets. For example, when we travel by metro it is essential for us that the interlocking system software controlling the metros are accurate so collisions and derailment are prevented. The reliability and safety of such interlocking systems are made on the precise functional requirements specification and verification respectively. Therefore, the precise functional requirements specification and verification of such interlocking systems represent a challenge in an active research area, so in this paper, we survey various articles in this field and discuss their consequences.

Modular specification and verification of closures in Rust

Closures are a language feature supported by many mainstream languages, combining the ability to package up references to code blocks with the possibility of capturing state from the environment of the closure's declaration. Closures are powerful, but complicate understanding and formal reasoning, especially when closure invocations may mutate objects reachable from the captured state or from closure arguments. This paper presents a novel technique for the modular specification and verification of closure-manipulating code in Rust. Our technique combines Rust's type system guarantees and novel specification features to enable formal verification of rich functional properties. It encodes higher-order concerns into a first-order logic, which enables automation via SMT solvers. Our technique is implemented as an extension of the deductive verifier Prusti, with which we have successfully verified many common idioms of closure usage.