As the scale and complexity of IoT systems continue to increase, communication security, mobile device design, and real-time data processing are under tremendous pressure, making it more challenging to build secure and reliable IoT systems. Therefore, there is an urgent need for rigorous theoretical specification and analysis of IoT systems, especially through formal methods. In response, our recent work proposed the Secure Mobile Real-time Process Calculus for Internet of Things (SMrCaIT) calculus, a process calculus designed for IoT systems. SMrCaIT is the calculus capable of comprehensively modeling the security, real-time, and mobility features of IoT systems. This article further explores how to predict and reason about program behavior using mathematical theory without actual execution, and how to formally describe equivalence relationships between programs. To achieve this, we define the denotational and algebraic semantics of the SMrCaIT calculus, based on the Unifying Theories of Programming (UTP). Additionally, to support the algebraic exploration of parallel expansion laws, we extend the SMrCaIT calculus with three types of guarded choices, enabling any SMrCaIT program to be transformed into a unified form (i.e., a guarded choice form). Finally, we use a Vehicle Ad Hoc Network (VANET) case to demonstrate the applicability of the denotational and algebraic semantics of the SMrCaIT calculus in real-world physical scenarios.
This article presents the collaborative European ESPRIT ProCoS projects on “Provably Correct Systems”, and associated initiatives of the 1990s. The influence of the projects in the field of formal methods is also discussed. A general overview of the projects is provided, together with a number of reminiscences by those involved with the projects, including the influence on the subsequent careers of participants. The projects addressed the issues of connecting formal approaches at different connected levels of formality, including requirements, specification, and compilation down to machine code and even directly into hardware. The investigations were based on a representative subset of the programming language Occam, which was subsequently extended by elements indicative of particular problems of compilation, yet not found in Occam, and the related Transputer microprocessor. In practice, two of the most important and enduring results after the projects were Duration Calculus and Unifying Theories of Programming, both subfields of formal methods, with associated communities of researchers and practitioners.
Reactive obstacle avoidance methods often cause agents to become trapped in local minima, because they can often only reason one step ahead (i.e., the next action based on the current state). In this paper, we use model checking to achieve reactive multi-step planning and obstacle avoidance on an autonomous robot. Our small, purpose-built model checking algorithm generates plans in situ (within the robot’s code) based on “core” knowledge and attention as found in biological agents. This is achieved in real-time using no pre-computed data on a low-powered device. Our approach is based on chaining temporary control systems that are spawned to counteract disturbances in the local environment which disrupt an autonomous agent from its preferred action (or resting state ). We mitigate state-space explosion by relying on temporary snapshots of the immediate environment, restricting the number of states. Multi-step planning using counter-examples generated by depth-first search and a negated LTL path property is applied to scenarios involving a cul-de-sac and a free-standing obstacle. Empirical results and informal proofs of two fundamental properties demonstrate the effectiveness of our approach for the creation of efficient multi-step plans for local obstacle avoidance. We significantly improve performance compared to a purely reactive agent that can only plan one step ahead. Our approach is an instructional case study for the development of safe and reliable navigation in the context of autonomous vehicles. We believe it also has general application in navigation for mission-critical mobile robots.
Formal methods are mathematically-based approaches with the potential to reveal hidden assumptions or overlooked requirements. Therefore, they provide means for precise specification, design, and verification of software and systems. Studying formal methods from a historical perspective preserves history, enables recognition of contributions, and investigates how local academic cultures, policies, and funding shaped their trajectories. This work fills the gap of the lack of a picture of the Brazilian formal methods community. It provides a historical narrative of this community in diverse dimensions, such as past and current research projects, research groups, teaching initiatives, and the profile of its flagship event. Through these contributions, we not only document the achievements and faced challenges, but also inspire future research and collaborations, underpinning the importance of formal methods in advancing software engineering practices in Brazil and beyond.
