Selected Publications |
Runtime Verification and Validation of Functional Reactive Systems
Authors: Ivan Perez (NIA / NASA Formal Methods Group); Henrik Nilsson (University of Nottingham)
Journal of Functional Programming, 30, E28. 2020.
(official)
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)
Authors: Ivan Perez (NIA / NASA Formal Methods Group); Alwyn Goodloe (NASA Langley Research Center)
Journal of Functional Programming, 30, E12. 2020.
(official)
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
Authors: Ivan Perez (NIA / NASA Formal Methods Group); Frank Dedden (Netherlands Aerospace Center); Alwyn Goodloe (NASA Langley Research Center)
NASA Technical Memorandum NASA/TM-2020-220587. 2020.
(official)
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 2018 - Co-located with ICFP 2018 (St Louis, USA)
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 2018 (St Louis, USA)
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 2017 - 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 2017 - 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 2017 (Oxford, UK)
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.
Haskell Symposium 2016 - Colocated with ICFP 2016
(Nara, Japan)
Authors: Ivan Perez, Manuel Bärenz
and Henrik Nilsson
(official)
(abstract)
(corrected
submission)
(implementation)
(errata)
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)
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.
Haskell Symposium 2015 - Colocated with ICFP 2015
(Vancouver, Canada)
Authors: Ivan Perez and Henrik Nilsson
(official)
(mirror)
(abstract)
(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
1st year PhD Report University of
Nottingham
(paper)
(bibtex)
(notes)
Includes an overview of GUI programming in
Haskell and FRP, Reactive Values and Relations.
Recommended for those who want to know more about the
current state of FRP.
Declarative Game Programming: Distilled
Tutorial
PPDP '14: International Symposium on Principles and
Practice of Declarative Programming
Authors: Henrik Nilsson and Ivan Perez
(abstract)
(bibtex)
(exdended
abstract)
Bridging the GUI Gap with Reactive Values and
Relations (superceeded)Trends in Functional
Programming 2014 - The Netherlands
Authors: Ivan Perez and Henrik Nilsson
(paper)
(bibtex)
|