Formal Specification Approach for Smart Space Development

Being an important application of the Internet of Things, smart spaces are increasingly developed throughout the world for different purposes ranging from home automation to smart grids. Despite the considerable focus given to the practical development of smart spaces, there are few attempts of utilizing formal methods in this domain. Especially, the requirements of developing a smart space have not yet been formally specified, to the best of the authors’ knowledge. To fill this gap, a formal specification approach is presented in this paper for smart space development. The proposed approach first identifies the key components of a smart space, then it uses a state-based formal specification language – Z, to formally specify the requirements of these components. The requirements of developing a hypothetical smart space are considered for formal specification in this paper. This work does not only demonstrate how the components of complex systems, such as smart spaces, can elegantly be modeled using a Software Engineering formalism. But it can also be used as a step towards defining a holistic smart space development framework, along with requirement engineering and system design techniques.

Modular Answer Set Programming as a Formal Specification Language

In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification.

The MINERVA Software Development Process

This paper presents a software development process for safety-critical software components of cyber-physical systems. The process is called MINERVA, which stands for Mirrored Implementation Numerically Evaluated against Rigorously Verified Algorithms. The process relies on formal methods for rigorously validating code against its requirements. The software development process uses: (1) a formal specification language for describing the algorithms and their functional requirements, (2) an interactive theorem prover for formally verifying the correctness of the algorithms, (3) test cases that stress the code, and (4) numerical evaluation on these test cases of both the algorithm specifications and their implementations in code. The MINERVA process is illustrated in this paper with an application to geo-containment algorithms for unmanned aircraft systems. These algorithms ensure that the position of an aircraft never leaves a predetermined polygon region and provide recovery maneuvers when the region is inadvertently exited.

E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper)

This tool paper presents E-ACSL, a runtime verification tool for C programs capable of checking a broad range of safety and security properties expressed using a formal specification language. E-ACSL consumes a C program annotated with formal specifications and generates a new C program that behaves similarly to the original if the formal properties are satisfied, or aborts its execution whenever a property does not hold. This paper presents an overview of E-ACSL and its specification language.