| Selected Publications |
Trustworthy Runtime Verification via Bisimulation (Experience Report)
28th ACM SIGPLAN International Conference on Functional Programming (ICFP 2023). 2023.
Authors: Ryan Scott, Mike Dodds, Ivan Perez, Alwyn Goodloe, Robert Dockins
(official)
(abstract)
When runtime verification is used to monitor safety-critical systems, it is essential that monitoring code behaves correctly. The Copilot runtime verification framework pursues this goal by automatically generating C monitor programs from a high-level DSL embedded in Haskell. In safety-critical domains, every piece of deployed code must be accompanied by an assurance argument that is convincing to human auditors. However, it is difficult for auditors to determine with confidence that a compiled monitor cannot crash and implements the behavior required by the Copilot semantics.
In this paper we describe CopilotVerifier, which runs alongside the Copilot compiler, generating a proof of correctness for the compiled output. The proof establishes that a given Copilot monitor and its compiled form produce equivalent outputs on equivalent inputs, and that they either crash in identical circumstances or cannot crash. The proof takes the form of a bisimulation broken down into a set of verification conditions. We leverage two pieces of SMT-backed technology: the Crucible symbolic execution library for LLVM and the What4 solver interface library. Our results demonstrate that dramatically increased compiler assurance can be achieved at moderate cost by building on existing tools. This paves the way to our ultimate goal of generating formal assurance arguments that are convincing to human auditors.
The Essence of Reactivity
16th ACM SIGPLAN International Haskell Symposium. 2023.
Authors: Ivan Perez, Frank Dedden
(official)
(abstract)
Reactive programming, functional reactive programming, event-based programming, stream programming, and temporal logic all share an underlying commonality: values can vary over time. These languages differ in multiple ways, including the nature of time itself (e.g., continuous or discrete, dense or sparse, implicit or explicit), on how much of the past and future can be referenced, on the kinds of values that can be represented, as well as the mechanisms used to evaluate expressions or formulas. This paper presents a series of abstractions that capture the essence of different forms of time variance. By separating the aspects that differentiate each family of formalisms, we can better express the commonalities and differences between them. We demonstrate our work with a prototype in Haskell that allows us to write programs in terms of a generic interface that can be later instantiated to different abstractions depending on the desired target.
Don't Go Down the Rabbit Hole: Reprioritizing Enumeration for Property-Based Testing
16th ACM SIGPLAN International Haskell Symposium. 2023.
Authors: Segev Elazar Mittelman, Aviel Resnick, Ivan Perez, Alwyn Goodloe, Leonidas Lampropoulos
(official)
(abstract)
Combinatorial testing is a popular software engineering technique for effectively testing programs that operate on parameters drawn from small, finite domains (such as configuration options), by providing a principled way of systematically exploring interactions between them. Property-based testing, on the other hand, is a widely used technique for testing the correctness of functional programs that usually operate on large, infinite domains (such as algebraic data types), by randomly generating or enumerating inputs.
In this paper, we show how to extend and apply ideas from the narrow scope of combinatorial testing techniques to the broader scope of property-based testing applications. In particular, we develop a novel way of pruning the input search space while still ensuring that a diverse set of constructor patterns appear among the set of generated tests. In our implementation, we integrate a state-of-the-art enumeration-based property-based testing framework, LazySearch, with a state-of-the-art combinatorial testing tool, NIST’s ACTS, and demonstrate how it can significantly speed up the effectiveness of testing—up to more than 20$ imes$ in the case of a prior System F case study from the literature.
Types that Change: The Extensible Type Design Pattern
ACM SIGPLAN Workshop on Functional Software Architecture - FP in the Large. 2023.
Authors: Ivan Perez
(official)
(abstract)
Compilers are often structured as chains of transformations, from source code to object code, through multiple intermediate representations. The existence of different representations of the same program presents challenges both for code maintenance and in terms of architecture. The types used to capture programs at multi- ple stages may be similar but not interchangeable, leading to code duplication. Methods to alleviate such duplication often lead to violations of software engineering principles of abstraction and encapsulation. This pearl discusses a design pattern where an algebraic data type (ADT) is extended with an argument type function that is applied to every component of the ADT. The resulting parametric type can be instantiated with multiple type functions, each providing a different feature. We demonstrate the versatility of this pattern by capturing notions of traceability and error recovery, and demonstrate that it can also be used to selectively modify existing types, as well as to extend them. Our proposal has been validated by applying it to a real-world use case with very good results.
The Beauty and Elegance of Functional Reactive Animation
11th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling and Design (FARM). 2023.
Authors: Ivan Perez
(official)
(abstract)
It has been over 20 years since Elliott and Hudak published Functional Reactive Animation, which outlined the principles of interactive programming in functional languages. As a result, Functional Reactive Programming (FRP) has seen numerous implementations and has been applied to multiple areas, like robotics, physics simulations, game programming and user interfaces. The use of the term FRP has itself broadened, and nowadays covers both continuous-time purely functional abstractions and discrete-time reactive implementations. This paper presents a series of increasingly complex FRP animations in a current implementation. With a main focus on clarity and meaning, we explore three independent dimensions: space, time, and color. We demonstrate that, when embraced fully, Functional Programming can result in declarative constructs that are aesthetically beautiful and notationally elegant.
Monitoring ROS2: from Requirements to Autonomous Robots
4th Workshop on Formal Methods for Autonomous Systems. 2022.
Authors: Ivan Perez, Anastasia Mavridou, Thomas Pressburger, Alexander Will, Patrick Martin
(official)
(abstract)
Runtime verification (RV) has the potential to enable the safe operation of safety-critical systems that are too complex to formally verify, such as Robot Operating System 2 (ROS2) applications. Writing correct monitors can itself be complex, and errors in the monitoring subsystem threaten the mission as a whole. This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool. FRET is used to specify requirements with unambiguous semantics, which are then automatically translated into temporal logic formulæ. Ogma generates monitor specifications from the FRET output, which are compiled into hard-real time C99. To facilitate integration of the monitors in ROS2, we have extended Ogma to generate ROS2 packages defining monitoring nodes, which run the monitors when new data becomes available, and publish the results of any violations. The goal of our approach is to treat the generated ROS2 packages as black boxes and integrate them into larger ROS2 systems with minimal effort.
Automated Translation of Natural Language Requirements to Runtime Monitors
28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2022.
Authors: Ivan Perez, Anastasia Mavridou, Thomas Pressburger, Alwyn Goodloe, Dimitra Giannakopoulou
(official)
(abstract)
Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. This paper presents an end-to-end framework to capture requirements in structured natural language and generate monitors that capture their semantics faithfully. We leverage NASA’s Formal Requirement Elicitation Tool (fret), and the RV system Copilot. We extend fret with mechanisms to capture additional information needed to generate monitors, and introduce Ogma, a new tool to bridge the gap between fret and Copilot. With this framework, users can write requirements in an intuitive format and obtain real-time C monitors suitable for use in embedded systems. Our toolchain is available as open source.
Integrating FRET with Copilot: Automated Translation of Natural Language Requirements to Runtime Monitors
NASA Technical Manual - NASA/TM-2022-0000049. 2022.
Authors: Ivan Perez, Anastasia Mavridou, Thomas Pressburger, Alwyn Goodloe, Dimitra Giannakopoulou
(official)
(abstract)
Runtime verification (RV) enables monitoring systems at runtime, to detect property violations early and limit their potential consequences. To provide the level of assurance required for ultra-critical systems, monitor specifications must faithfully reflect the original mission requirements, which are often written in ambiguous natural language. This paper presents an end-to-end framework to capture requirements in structured natural language and generate monitors that capture their semantics faithfully. We leverage NASA’s Formal Requirement Elicitation Tool (FRET), and the RV system Copilot. We extend FRET with mechanisms to capture additional information needed to generate monitors, and introduce OGMA, a new tool to bridge the gap between FRET and Copilot. With this framework, users can write requirements in an intuitive format and obtain real-time C monitors suitable for use in embedded systems. Our tool chain is available as open source.
From Requirements to Autonomous Flight: An Overview of the Monitoring ICAROUS Project
In Proceedings Second Workshop on Formal Methods for Autonomous Systems, EPTCS 329. 2020.
Authors: Aaron Dutle, Cesar Munoz, Esther Conrad, Alwyn Goodloe, Laura Titolo, Ivan Perez, Swee Balachandran, Dimitra Giannakopoulou, Anastasia Mavridou, Thomas Pressburger
(official)
(abstract)
The Independent Configurable Architecture for Reliable Operations of Unmanned Systems (ICAROUS) is a software architecture incorporating a set of algorithms to enable autonomous operations of unmanned aircraft applications. This paper provides an overview of Monitoring ICAROUS, a project whose objective is to provide a formal approach to generating runtime monitors for autonomous systems from requirements written in a structured natural language. This approach integrates FRET, a formal requirement elicitation and authoring tool, and Copilot, a runtime verification framework. FRET is used to specify formal requirements in structured natural language. These requirements are translated into temporal logic formulae. Copilot is then used to generate executable runtime monitors from these temporal logic specifications. The generated monitors are directly integrated into ICAROUS to perform runtime verification during flight.
Runtime Verification and Validation of Functional Reactive Systems
Journal of Functional Programming, 30, E28. 2020.
Authors: Ivan Perez (NIA / NASA Formal Methods Group); Henrik Nilsson (University of Nottingham)
(official)
(abstract)
Many types of interactive applications, including reactive systems implemented in hardware, interactive physics simulations and games, raise particular challenges when it comes to testing and debugging. Reasons include de facto lack of reproducibility and difficulties of automatically generating suitable test data. This paper demonstrates that certain variants of functional reactive programming (FRP) implemented in pure functional languages can mitigate such difficulties by offering referential transparency at the level of whole programs. This opens up for a multi-pronged approach for assisting with testing and debugging that works across platforms, including assertions based on temporal logic, recording and replaying of runs (also from deployed code), and automated random testing using QuickCheck. When combined with extensible forms of FRP that allow for constrained side effects, it allows us to not only validate software simulations but to analyse the effect of faults in reactive systems, confirm the efficacy of fault tolerance mechanisms and perform software- and hardware-in-the-loop testing. The approach has been validated on non-trivial systems implemented in several existing FRP implementations, by means of careful debugging using a tool that allows the test or simulation under scrutiny to be controlled, moving along the execution time line, and pin-pointing of violations of assertions on personal computers as well as external devices.
Fault-tolerant functional reactive programming (extended version)
Journal of Functional Programming, 30, E12. 2020.
Authors: Ivan Perez (NIA / NASA Formal Methods Group); Alwyn Goodloe (NASA Langley Research Center)
(official)
(abstract)
Highly critical application domains, like medicine and aerospace, require the use of strict design, implementation, and validation techniques. Functional languages have been used in these domains to develop synchronous dataflow programming languages for reactive systems. Causal stream functions and functional reactive programming (FRP) capture the essence of those languages in a way that is both elegant and robust. To guarantee that critical systems can operate under high stress over long periods of time, these applications require clear specifications of possible faults and hazards, and how they are being handled. Modeling failure is straightforward in functional languages, and many functional reactive abstractions incorporate support for failure or termination. However, handling unknown types of faults, and incorporating fault tolerance into FRP, requires a different construction and remains an open problem. This work demonstrates how to extend an existing functional reactive framework with fault tolerance features. At value level, we tag faulty signals with reliability and probability information and use random testing to inject faults and validate system properties encoded in temporal logic. At type level, we tag components with the kinds of faults they may exhibit and use type-level programming to obtain compile-time guarantees of key aspects of fault tolerance. Our approach is powerful enough to be used in systems with realistic complexity, and flexible enough to be used to guide system analysis and design, validate system properties in the presence of faults, perform runtime monitoring, and study the effects of different fault tolerance mechanisms.
Copilot 3
NASA Technical Memorandum NASA/TM-2020-220587. 2020.
Authors: Ivan Perez (NIA / NASA Formal Methods Group); Frank Dedden (Netherlands Aerospace Center); Alwyn Goodloe (NASA Langley Research Center)
(official)
(abstract)
Ultra-critical systems require high-level assurance, which cannot always be guaranteed in compile time. The use of runtime verification (RV) enables monitoring these systems in runtime, to detect property violations early and limit their potential consequences. The introduction of monitors in ultra-critical systems poses a challenge, as failures and delays in the RV subsystem could affect other subsystems and threaten the mission as a whole. This paper presents Copilot 3, a runtime verification framework for real-time embedded systems. Copilot monitors are written in a compositional, stream-based language with support for a variety of Temporal Logics (TL), which results in robust, high-level specifications that are easier to understand than their traditional counterparts. The framework translates monitor specifications into C code with static memory requirements, which can be compiled to run on embedded hardware. This paper presents version 3 of the Copilot language, demonstrates its suitability with a number of examples, and discusses its use in larger applications. Additionally, it describes the framework?s architecture, its implementation as a Domain Specific Language (DSL) embedded in Haskell, and the progress of the project over the years.
Fault-Tolerant Swarms
Space Mission Challenges in Information Technology (SMC-IT) (Caltech, California, USA). 2019.
Authors: Ivan Perez (NIA / NASA Formal Methods Group); Alwyn Goodloe (NASA Langley Research Center); William Edmonson (NCAT)
(official)
(abstract)
Safety-critical systems must be engineered to be ultra-reliable. Redundancy is critical to tolerate faults that cannot be eliminated by using ruggedized or hardened computing. The use of small satellites allows new missions to be cost-effective, but it also introduces new problems in terms of robustness and fault handling. Apart from the inherent problems of working in a distributed setting, small sats normally lack the redundancy needed to deal with pernicious faults due to constraints on weight, cost and complexity. This paper presents and evaluates fault tolerance mechanisms in a swarm of satellites considered as a whole, making it robust to the failure of one or more satellites. The evaluation is performed with a computer model augmented with the properties desired from our system. We use a random testing tool to inject faults in different parts of our model and evaluate the fault detection and fault correction mechanisms we propose. Our results support the suitability of the proposed fault model, fault tolerant architecture, and evaluation methodology.
Formal Verification of System States for Spacecraft Automatic Maneuvering
AIAA SciTech Forum (2019-1187) (San Diego, California, USA). 2019.
Authors: Kerianne L. Hobbs (Air Force Research Laboratory); Ivan Perez (NIA / NASA Formal Methods Group); Aaron Fifarek (LinQuest Corporation); Eric M. Feron (Georgia Tech)
(official)
(abstract)
As the complexity and number of space operations in Earth orbit continues to grow, there are increased opportunities to incorporate automatic or autonomous maneuvering as part of a space traffic management framework. Understanding the context of the automatic maneuver, including the conditions under which an automatic maneuver is acceptable, is important to the design of the overall automatic maneuver system. This work proposes and conducts formal verification of high-level system requirements to govern automatic maneuvering of satellites in the presence of safety interlocks or failures. Three examples of automatic maneuver contexts are considered: conjunction avoidance, especially in the presence of orbital debris; rendezvous and proximity operations, especially for service satellites and active debris removal; and station keeping, especially in large satellite constellations providing space-based services like Internet. The primary contribution of this paper is the development and analysis of formal requirements for high-level system states governing when an automatic maneuver is acceptable. The requirements serve as a baseline framework for future automatic spacecraft maneuver research.
Rhine: FRP with Type-Level Clocks
Haskell Symposium - Co-located with ICFP (St Louis, USA). 2018.
Authors: Manuel Bärenz and Ivan Perez
(official)
(abstract)
Processing data at different rates is generally a hard problem in reactive programming. Buffering problems, lags, and concurrency issues often occur. Many of these problems are clock errors, where data at different rates is combined incorrectly. Techniques to avoid clock errors, such as type-level clocks and deterministic scheduling, exist in the field of synchronous programming, but are not implemented in general-purpose languages like Haskell.
Rhine is a clock-safe library for synchronous and asynchronous Functional Reactive Programming (FRP). It separates the aspects of clocking, scheduling and resampling from each other, and ensures clock-safety at the type level. Concurrent communication is encapsulated safely. Diverse reactive subsystems can be combined in a coherent, declarative data-flow framework, while correct interoperability of data at different rates is guaranteed by type-level clocks.
This provides a general-purpose framework that simplifies multi-rate FRP systems and can be used for game development, media applications, GUIs and embedded systems, through a flexible API with many reusable components.
Fault Tolerant Functional Reactive Programming
ICFP (St Louis, USA). 2018.
Authors: Ivan Perez
(official)
(abstract)
Highly critical application domains, like medicine and aerospace, require the use of strict design, implementation and validation techniques. Functional languages have been used in these domains to develop synchronous dataflow programming languages for reactive systems. Causal stream functions and Functional Reactive Programming capture the essence of those languages in a way that is both elegant and robust.
To guarantee that critical systems can operate under high stress over long periods of time, these applications require clear specifications of possible faults and hazards, and how they are being handled. Modeling failure is straightforward in functional languages, and many Functional Reactive abstractions incorporate support for failure or termination. However, handling unknown types of faults, and incorporating fault tolerance into Functional Reactive Programming, requires a different construction and remains an open problem.
This work presents extensions to an existing functional reactive abstraction to facilitate tagging reactive transformations with hazard tags or confidence levels. We present a prototype framework to quantify the reliability of a reactive construction, by means of numeric factors or probability distributions, and demonstrate how to aid the design of fault-tolerant systems, by constraining the allowed reliability to required boundaries. By applying type-level programming, we show that it is possible to improve static analysis and have compile-time guarantees of key aspects of fault tolerance. Our approach is powerful enough to be used in systems with realistic complexity, and flexible enough to be used to guide their analysis and design, to test system properties, to verify fault tolerance properties, to perform runtime monitoring, to implement fault tolerance during execution and to address faults during runtime. We present implementations in Haskell and in Idris.
GALE: a functional Graphic Adventure Library and Engine
FARM - Colocated with ICFP. 2017.
Authors: Ivan Perez
(official)
(abstract)
Functional Programming brings a promise of highly-declarative code, efficient, parallelisable execution, modularity and reusability. In spite of these advantages, the use of pure Functional Languages in commercial games is still rare. This is partially caused lack of backends for multimedia, lack of production tools, and the demon- stration that functional abstractions work for other than non-trivial examples. In this paper we present GALE, a Graphic Adventure Library and Engine implemented in Haskell. Our engine implements the basic common features available in similar commercial engines for graphic adventures. We show a high-level abstract definition of game descriptions that allows us not only to run them, but also to analyse them in compile time. We also demonstrate how this description allows us to provide novel features not available in traditional engines. Our system works on iOS, Android and desktop, and is accompanied by a development environment to compose the games with no prior programming skills.
Back to the Future: Time Travel in FRP
Haskell Symposium - Colocated with ICFP. 2017.
Authors: Ivan Perez
(official)
(abstract)
Functional Reactive Programming (FRP) allows interactive applications to be modelled in a declarative manner using time-varying values. For practical reasons, however, operational constraints are often imposed, such as having a fixed time domain, time always flowing forward, and limiting the exploration of the past. In this paper we show how these constraints can be overcome, giving local control over the time domain, the direction of time and the sampling step. We study the behaviour of FRP expressions when time flows backwards, and demonstrate how to synchronize subsystems running asynchronously and at different sampling rates. We have verified the practicality of our approach with two non-trivial games in which time control is central to the gameplay.
Testing and Debugging Functional Reactive Programming
ICFP (Oxford, UK). 2017.
Authors: Ivan Perez and Henrik Nilsson
(official)
(abstract)
Many types of interactive applications, including video games, raise particular challenges when it comes to testing and debugging. Reasons include de-facto lack of reproducibility and difficulties of automatically generating suitable test data. This paper demonstrates that certain variants of Functional Reactive Programming (FRP) implemented in pure functional languages can mitigate such difficulties by offering referential transparency at the level of whole programs. This opens up for a multi-pronged approach for assisting with testing and debugging that works across platforms, including assertions based on temporal logic, recording and replaying of runs (also from deployed code), and automated random testing using QuickCheck. The approach has been validated on real, non-trivial games implemented in the FRP system Yampa through a tool providing a convenient Graphical User Interface that allows the execution of the code under scrutiny to be controlled, moving along the execution time line, and pin-pointing of violations of assertions on PCs as well as mobile platforms.
Functional Reactive Programming, Refactored
Haskell Symposium - Colocated with ICFP (Nara, Japan). 2017.
Authors: Ivan Perez, Manuel Bärenz and Henrik Nilsson
(official)
(corrected submission)
(implementation)
(errata)
(abstract)
Functional Reactive Programming (FRP) has come to mean many things. Yet, scratch the surface of the multitude of realisations, and there is great commonality between them. This paper investigates this commonality, turning it into a mathematically coherent and practical FRP realisation that allows us to express the functionality of many existing FRP systems and beyond by providing a minimal FRP core parametrised on a monad. We give proofs for our theoretical claims and we have verified the practical side by benchmarking a set of existing, non-trivial Yampa applications running on top of our new system with very good results.
On the Mathematical Properties of Monadic Stream Functions
(Draft). 2016.
Authors: Manuel Bärenz, Ivan Perez, and Henrik Nilsson
(paper)
(abstract)
Monadic Stream Functions are CPS functions parameterised over a monadic context. They form a suitable abstraction to describe reactive processes, but what properties do they fulfill? In this technical report we explore some of the properties of Monadic Stream Functions, in particular those related to Arrows and Causal Commutative Arrows.
Bridging the GUI Gap with Reactive Values and Relations
Haskell Symposium - Colocated with ICFP (Vancouver, Canada). 2015.
Authors: Ivan Perez and Henrik Nilsson
(official)
(mirror)
(bibtex)
(abstract)
Reactive Values are an abstraction for mutable elements with a change-propagation or notification mechanism. They enable abstract reactive programming by hiding details on how to access particular values, how to deal with concurrency, etc. They provide a uniform interface for GUI widget properties, application models (in MVC terminology), hardware, files, etc. Reactive Values can be connected to one another forming uni- or bi-directional Reactive Relations. For an implementation, see: Keera Hails
Declarative Game Programming: Distilled Tutorial
PPDP '14: International Symposium on Principles and Practice of Declarative Programming. 2014.
Authors: Henrik Nilsson and Ivan Perez
(abstract)
(bibtex)
(exdended abstract)
|
