-
Matthew Chan,
Daniel Ricketts,
Sorin Lerner,
and Gregory Malecha.
Formal Verification of Stability Properties of Cyber-Physical Systems.
pp 2,
2016.
Keyword(s): Coq,
verification.
@article{chanFormalVerificationStability2016,
title = {Formal {{Verification}} of {{Stability Properties}} of {{Cyber}}-Physical {{Systems}}},
author = {Chan, Matthew and Ricketts, Daniel and Lerner, Sorin and Malecha, Gregory},
year = {2016},
pages = {2},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4259-Chan et al - Formal Veriï¬cation of Stability Properties of Cyber-physical Systems.pdf},
keywords = {Coq,verification},
}
-
Robert Kelly,
Barak A. Pearlmutter,
and Jeffrey Mark Siskind.
Evolving the Incremental Lambda Calculus into a Model of Forward Automatic Differentiation (AD).
arXiv:1611.03429 [cs],
November 2016.
Keyword(s): calculus.
Abstract: |
Formal transformations somehow resembling the usual derivative are surprisingly common in computer science, with two notable examples being derivatives of regular expressions and derivatives of types. A newcomer to this list is the incremental \$ extbackslash lambda\$-calculus, or ILC, a "theory of changes" that deploys a formal apparatus allowing the automatic generation of efficient update functions which perform incremental computation. The ILC is not only defined, but given a formal machine-understandable definition---accompanied by mechanically verifiable proofs of various properties, including in particular correctness of various sorts. Here, we show how the ILC can be mutated into propagating tangents, thus serving as a model of Forward Accumulation Mode Automatic Differentiation. This mutation is done in several steps. These steps can also be applied to the proofs, resulting in machine-checked proofs of the correctness of this model of forward AD. |
@article{kellyEvolvingIncrementalLambda2016,
title = {Evolving the {{Incremental}} {{Lambda}} {{Calculus}} into a {{Model}} of {{Forward Automatic Differentiation}} ({{AD}})},
author = {Kelly, Robert and Pearlmutter, Barak A. and Siskind, Jeffrey Mark},
year = {2016},
month = nov,
abstract = {Formal transformations somehow resembling the usual derivative are surprisingly common in computer science, with two notable examples being derivatives of regular expressions and derivatives of types. A newcomer to this list is the incremental \$ extbackslash lambda\$-calculus, or ILC, a "theory of changes" that deploys a formal apparatus allowing the automatic generation of efficient update functions which perform incremental computation. The ILC is not only defined, but given a formal machine-understandable definition---accompanied by mechanically verifiable proofs of various properties, including in particular correctness of various sorts. Here, we show how the ILC can be mutated into propagating tangents, thus serving as a model of Forward Accumulation Mode Automatic Differentiation. This mutation is done in several steps. These steps can also be applied to the proofs, resulting in machine-checked proofs of the correctness of this model of forward AD.},
archivePrefix = {arXiv},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4526 - Kelly et al (2016) - Evolving the Incremental -lambda Calculus into a Model of Forward Automatic.pdf},
journal = {arXiv:1611.03429 [cs]},
keywords = {calculus},
}
-
Stefan Mitsch and André Platzer.
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models.
Formal Methods in System Design,
49(1):33-74,
October 2016.
ISSN: 1572-8102.
Keyword(s): verification.
Abstract: |
Formal verification and validation play a crucial role in making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified with respect to the model. Otherwise, all bets are off. This article introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures in a provably correct way that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions, assuming the system dynamics deviation is bounded. This article, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic by a correct-by-construction approach, leading to verifiably correct runtime model validation. Overall, ModelPlex generates provably correct monitor conditions that, if checked to hold at runtime, are provably guaranteed to imply that the offline safety verification results about the CPS model apply to the present run of the actual CPS implementation. |
@article{mitschModelPlexVerifiedRuntime2016,
title = {{{ModelPlex}}: Verified Runtime Validation of Verified Cyber-Physical System Models},
author = {Mitsch, Stefan and Platzer, Andr{\'e}},
year = {2016},
month = oct,
volume = {49},
pages = {33--74},
issn = {1572-8102},
doi = {10.1007/s10703-016-0241-z},
abstract = {Formal verification and validation play a crucial role in making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified with respect to the model. Otherwise, all bets are off. This article introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures in a provably correct way that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions, assuming the system dynamics deviation is bounded. This article, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic by a correct-by-construction approach, leading to verifiably correct runtime model validation. Overall, ModelPlex generates provably correct monitor conditions that, if checked to hold at runtime, are provably guaranteed to imply that the offline safety verification results about the CPS model apply to the present run of the actual CPS implementation.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4178-Mitsch_Platzer (2016) - ModelPlex.pdf},
journal = {Formal Methods in System Design},
keywords = {verification},
number = {1}
}
-
Johannes Borgström,
Ugo Dal Lago,
Andrew D. Gordon,
and Marcin Szymczak.
A Lambda-Calculus Foundation for Universal Probabilistic Programming.
In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming - ICFP 2016,
Nara, Japan,
pages 33-46,
2016.
ACM Press.
ISBN: 978-1-4503-4219-3.
Keyword(s): calculus,
probability.
Abstract: |
We develop the operational semantics of an untyped probabilistic {$\lambda$}-calculus with continuous distributions, and both hard and soft constraints, as a foundation for universal probabilistic programming languages such as CHURCH, ANGLICAN, and VENTURE. Our first contribution is to adapt the classic operational semantics of {$\lambda$}-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints. |
@inproceedings{borgstromLambdacalculusFoundationUniversal2016,
title = {A Lambda-Calculus Foundation for Universal Probabilistic Programming},
booktitle = {Proceedings of the 21st {{ACM SIGPLAN International Conference}} on {{Functional Programming}} - {{ICFP}} 2016},
author = {Borgstr{\"o}m, Johannes and Dal Lago, Ugo and Gordon, Andrew D. and Szymczak, Marcin},
year = {2016},
pages = {33--46},
publisher = {{ACM Press}},
address = {{Nara, Japan}},
doi = {10.1145/2951913.2951942},
abstract = {We develop the operational semantics of an untyped probabilistic {$\lambda$}-calculus with continuous distributions, and both hard and soft constraints, as a foundation for universal probabilistic programming languages such as CHURCH, ANGLICAN, and VENTURE. Our first contribution is to adapt the classic operational semantics of {$\lambda$}-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4403-Borgstrom et al (2016) - A lambda-calculus foundation for universal probabilistic programming.pdf},
isbn = {978-1-4503-4219-3},
keywords = {calculus,probability},
}
-
Maria Consiglio,
Cesar Munoz,
George Hagen,
Anthony Narkawicz,
and Swee Balachandran.
ICAROUS: Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems.
In 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC),
Sacramento, CA, USA,
pages 1-5,
September 2016.
IEEE.
ISBN: 978-1-5090-2523-7.
Keyword(s): avionics,
verification.
Abstract: |
NASA's Unmanned Aerial System (UAS) Traffic Management (UTM) project aims at enabling near-term, safe operations of small UAS vehicles in uncontrolled airspace, i.e., Class G airspace. A far-term goal of UTM research and development is to accommodate the expected rise in small UAS traffic density throughout the National Airspace System (NAS) at low altitudes for beyond visual line-of-sight operations. This paper describes a new capability referred to as ICAROUS (Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems), which is being developed under the UTM project. ICAROUS is a software architecture comprised of highly assured algorithms for building safety-centric, autonomous, unmanned aircraft applications. Central to the development of the ICAROUS algorithms is the use of well-established formal methods to guarantee higher levels of safety assurance by monitoring and bounding the behavior of autonomous systems. The core autonomy-enabling capabilities in ICAROUS include constraint conformance monitoring and contingency control functions. ICAROUS also provides a highly configurable user interface that enables the modular integration of mission-specific software components. |
@inproceedings{consiglioICAROUSIntegratedConfigurable2016,
title = {{{ICAROUS}}: {{Integrated}} Configurable Algorithms for Reliable Operations of Unmanned Systems},
booktitle = {2016 {{IEEE}}/{{AIAA}} 35th {{Digital Avionics Systems Conference}} ({{DASC}})},
author = {Consiglio, Maria and Munoz, Cesar and Hagen, George and Narkawicz, Anthony and Balachandran, Swee},
year = {2016},
month = sep,
pages = {1--5},
publisher = {{IEEE}},
address = {{Sacramento, CA, USA}},
doi = {10.1109/DASC.2016.7778033},
abstract = {NASA's Unmanned Aerial System (UAS) Traffic Management (UTM) project aims at enabling near-term, safe operations of small UAS vehicles in uncontrolled airspace, i.e., Class G airspace. A far-term goal of UTM research and development is to accommodate the expected rise in small UAS traffic density throughout the National Airspace System (NAS) at low altitudes for beyond visual line-of-sight operations. This paper describes a new capability referred to as ICAROUS (Integrated Configurable Algorithms for Reliable Operations of Unmanned Systems), which is being developed under the UTM project. ICAROUS is a software architecture comprised of highly assured algorithms for building safety-centric, autonomous, unmanned aircraft applications. Central to the development of the ICAROUS algorithms is the use of well-established formal methods to guarantee higher levels of safety assurance by monitoring and bounding the behavior of autonomous systems. The core autonomy-enabling capabilities in ICAROUS include constraint conformance monitoring and contingency control functions. ICAROUS also provides a highly configurable user interface that enables the modular integration of mission-specific software components.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4272-Consiglio et al (2016) - ICAROUS.pdf},
isbn = {978-1-5090-2523-7},
keywords = {avionics,verification},
}
-
Gregory Malecha,
Daniel Ricketts,
Mario M. Alvarez,
and Sorin Lerner.
Towards Foundational Verification of Cyber-Physical Systems.
In 2016 Science of Security for Cyber-Physical Systems Workshop (SOSCYPS),
Vienna, Austria,
pages 1-5,
April 2016.
IEEE.
ISBN: 978-1-5090-4304-0.
Keyword(s): verification.
Abstract: |
The safety-critical aspects of cyber-physical systems motivate the need for rigorous analysis of these systems. In the literature this work is often done using idealized models of systems where the analysis can be carried out using highlevel reasoning techniques such as Lyapunov functions and model checking. In this paper we present VERIDRONE, a foundational framework for reasoning about cyber-physical systems at all levels from high-level models to C code that implements the system. VERIDRONE is a library within the Coq proof assistant enabling us to build on its foundational implementation, its interactive development environments, and its wealth of libraries capturing interesting theories ranging from real numbers and differential equations to verified compilers and floating point numbers. These features make proof assistants in general, and Coq in particular, a powerful platform for unifying foundational results about safetycritical systems and ensuring interesting properties at all levels of the stack. |
@inproceedings{malechaFoundationalVerificationCyberphysical2016,
title = {Towards Foundational Verification of Cyber-Physical Systems},
booktitle = {2016 {{Science}} of {{Security}} for {{Cyber}}-{{Physical Systems Workshop}} ({{SOSCYPS}})},
author = {Malecha, Gregory and Ricketts, Daniel and Alvarez, Mario M. and Lerner, Sorin},
year = {2016},
month = apr,
pages = {1--5},
publisher = {{IEEE}},
address = {{Vienna, Austria}},
doi = {10.1109/SOSCYPS.2016.7580000},
abstract = {The safety-critical aspects of cyber-physical systems motivate the need for rigorous analysis of these systems. In the literature this work is often done using idealized models of systems where the analysis can be carried out using highlevel reasoning techniques such as Lyapunov functions and model checking. In this paper we present VERIDRONE, a foundational framework for reasoning about cyber-physical systems at all levels from high-level models to C code that implements the system. VERIDRONE is a library within the Coq proof assistant enabling us to build on its foundational implementation, its interactive development environments, and its wealth of libraries capturing interesting theories ranging from real numbers and differential equations to verified compilers and floating point numbers. These features make proof assistants in general, and Coq in particular, a powerful platform for unifying foundational results about safetycritical systems and ensuring interesting properties at all levels of the stack.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4225-Malecha et al (2016) - Towards foundational verification of cyber-physical systems.pdf},
isbn = {978-1-5090-4304-0},
keywords = {verification},
}
-
Muhammad Qasim,
Osman Hasan,
Maissa Elleuch,
and Sofiène Tahar.
Formalization of Normal Random Variables in HOL.
In Michael Kohlhase,
Moa Johansson,
Bruce Miller,
Leonardo de Moura,
and Frank Tompa, editors,
Intelligent Computer Mathematics,
Lecture Notes in Computer Science,
Cham,
pages 44-59,
2016.
Springer International Publishing.
ISBN: 978-3-319-42547-4.
Keyword(s): HOL,
probability.
Abstract: |
Many components of engineering systems exhibit random and uncertain behaviors that are normally distributed. In order to conduct the analysis of such systems within the trusted kernel of a higher-order-logic theorem prover, in this paper, we provide a higher-order-logic formalization of Lebesgue measure and Normal random variables along with the proof of their classical properties. To illustrate the usefulness of our formalization, we present a formal analysis of the probabilistic clock synchronization in wireless sensor networks. |
@inproceedings{qasimFormalizationNormalRandom2016,
title = {Formalization of {{Normal Random Variables}} in {{HOL}}},
booktitle = {Intelligent {{Computer Mathematics}}},
author = {Qasim, Muhammad and Hasan, Osman and Elleuch, Maissa and Tahar, Sofi{\`e}ne},
editor = {Kohlhase, Michael and Johansson, Moa and Miller, Bruce and {de Moura}, Leonardo and Tompa, Frank},
year = {2016},
pages = {44--59},
publisher = {{Springer International Publishing}},
address = {{Cham}},
doi = {10.1007/978-3-319-42547-4_4},
abstract = {Many components of engineering systems exhibit random and uncertain behaviors that are normally distributed. In order to conduct the analysis of such systems within the trusted kernel of a higher-order-logic theorem prover, in this paper, we provide a higher-order-logic formalization of Lebesgue measure and Normal random variables along with the proof of their classical properties. To illustrate the usefulness of our formalization, we present a formal analysis of the probabilistic clock synchronization in wireless sensor networks.},
isbn = {978-3-319-42547-4},
keywords = {HOL,probability},
series = {Lecture {{Notes}} in {{Computer Science}}}
}
-
Daniel Ricketts,
Gregory Malecha,
and Sorin Lerner.
Modular Deductive Verification of Sampled-Data Systems.
In Proceedings of the 13th International Conference on Embedded Software - EMSOFT '16,
Pittsburgh, Pennsylvania,
pages 1-10,
2016.
ACM Press.
ISBN: 978-1-4503-4485-2.
Keyword(s): verification.
Abstract: |
Unsafe behavior of cyber-physical systems can have disastrous consequences, motivating the need for formal verification of these kinds of systems. Deductive verification in a proof assistant such as Coq is a promising technique for this verification because it (1) justifies all verification from first principles, (2) is not limited to classes of systems for which full automation is possible, and (3) provides a platform for proving powerful, higher-order modularity theorems that are crucial for scaling verification to complex systems. In this paper, we demonstrate the practicality, utility, and scalability of this approach by developing in Coq sound and powerful rules for modular construction and verification of sampleddata cyber-physical systems. We evaluate these rules by using them to verify a number of non-trivial controllers enforcing safety properties of a quadcopter, e.g. a geo-fence. We show that our controllers are realistic by running them on a real, flying quadcopter. |
@inproceedings{rickettsModularDeductiveVerification2016,
title = {Modular Deductive Verification of Sampled-Data Systems},
booktitle = {Proceedings of the 13th {{International Conference}} on {{Embedded Software}} - {{EMSOFT}} '16},
author = {Ricketts, Daniel and Malecha, Gregory and Lerner, Sorin},
year = {2016},
pages = {1--10},
publisher = {{ACM Press}},
address = {{Pittsburgh, Pennsylvania}},
doi = {10.1145/2968478.2968495},
abstract = {Unsafe behavior of cyber-physical systems can have disastrous consequences, motivating the need for formal verification of these kinds of systems. Deductive verification in a proof assistant such as Coq is a promising technique for this verification because it (1) justifies all verification from first principles, (2) is not limited to classes of systems for which full automation is possible, and (3) provides a platform for proving powerful, higher-order modularity theorems that are crucial for scaling verification to complex systems. In this paper, we demonstrate the practicality, utility, and scalability of this approach by developing in Coq sound and powerful rules for modular construction and verification of sampleddata cyber-physical systems. We evaluate these rules by using them to verify a number of non-trivial controllers enforcing safety properties of a quadcopter, e.g. a geo-fence. We show that our controllers are realistic by running them on a real, flying quadcopter.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4250-Ricketts et al (2016) - Modular deductive verification of sampled-data systems.pdf},
isbn = {978-1-4503-4485-2},
keywords = {verification},
}