diff --git a/WC-End2End/CompCert.tex b/WC-End2End/CompCert.tex deleted file mode 100644 index 5af6aeb..0000000 --- a/WC-End2End/CompCert.tex +++ /dev/null @@ -1,5 +0,0 @@ -\section{Turtles All The Way Down}~\label{sec:compcert} - -How we leverage the compcert compiler when possible. - - diff --git a/WC-End2End/conclusion.tex b/WC-End2End/conclusion.tex deleted file mode 100644 index 87e2d53..0000000 --- a/WC-End2End/conclusion.tex +++ /dev/null @@ -1,3 +0,0 @@ -\section{Conclusion}~\label{sec:conclusion} - -Conclusion diff --git a/WC-End2End/copilot.tex b/WC-End2End/copilot.tex deleted file mode 100644 index 3b528aa..0000000 --- a/WC-End2End/copilot.tex +++ /dev/null @@ -1,78 +0,0 @@ -\section{Copilot RV Framework}~\label{sec:Copilot} - -% A short introduction to the copilot language and framework. - -Copilot is a language tailored to developing runtime monitors for hard -real-time, distributed, reactive systems. Briefly, a runtime monitor is a -program that runs concurrently with a target program with the sole purpose of -assuring that the target program behaves in accordance with a pre-established -specification\citep{monitors}. Copilot is a language for writing such -specifications\citep{copilot, pike-icfp-12, pike-isse-13}. It is an embedded -domain-specific language, hosted in the lazy functional programming language -Haskell. - - - \begin{figure}[ht!] - \centering - \footnotesize - \begin{tikzpicture}[->, node distance=2.6cm, auto, shorten >=1pt, bend angle=45, - thick] - \tikzstyle{every state}=[rectangle, rounded corners] - - - \node[state] (Int) {Interpreter}; - \node[state] (Lang) [above right of=Int] - { - \begin{tabular}[b]{l} - Copilot Libraries\\ \hline Copilot Language - \end{tabular}}; - - \node[state] (M4) [left=3cm of Lang] {M4}; - \node[state] (Core) [below right of=Lang] {Copilot Core}; - \node[state] (PP) [right of=Core] {Pretty Printer}; - - - \node[state] (ACSL) [below of=PP] {\begin{tabular}[b]{l} - ACSL\\ generator - \end{tabular}}; - \node[state] (DOTc) [right of=ACSL] {\begin{tabular}[b]{l} - DOT\\ generator - \end{tabular}}; - \node[state] (SMTlib) [right of=DOTc] {\begin{tabular}[b]{l} - SMTlib\\ generator - \end{tabular}}; - \node[state] (Z3) [below of=SMTlib] {Z3}; - \node[state] (SBV) [below of=Core] {SBV Back-End}; - \node[state] (C99S) [below of=SBV] {\begin{tabular}[b]{l} - DOT\\ \hline ACSL\\ \hline C99 - \end{tabular}}; - \node[state] (DOT) [below right of=C99S] {DOT/graphviz}; - \node[state] (CCOMP) [below left=0.3cm and 0.3cm of C99S] {CompCert}; - \node[state] (ASM) [below=1cm of CCOMP] {Assembly code}; - - - \tikzstyle{every node}=[] - - - \path %% (Libs) edge node {0,1,L} (Lang); - (Lang) edge [bend left, anchor=west, text width=2.5cm] node {Reification and DSL-specific type-checking} (Core) - (M4) edge [text width=2.5cm] node {Preprocessing} (Lang) - (Core) edge [anchor=east] node {Translation} (SBV) - edge node {} (PP) - edge node [swap] {Evaluation} (Int) - (ACSL) edge [bend left, anchor=west] node {Integration} (C99S) - (DOTc) edge [bend left, anchor=east] node {} (C99S) - %(Int) edge [<->, bend right, anchor=east] node {QuickCheck} (SBV) - (PP) edge [->, anchor=east] node {ACSL gen.} (ACSL) - (PP) edge [->, anchor=north] node {DOT gen.} (DOTc) - (PP) edge [->, anchor=west] node {SMTlib generation} (SMTlib) - (SMTlib) edge [->, anchor=west] node {theorem prooving} (Z3) - (C99S) edge [->, anchor=north west] node {make} (CCOMP) - (CCOMP) edge [->, anchor=east] node {Cross-compilation} (ASM) - (C99S) edge [loop left, ->, anchor=east] node {Verification with frama-c WP plugin} (C99S) - (C99S) edge [->, anchor=west] node {Extraction and graph generation} (DOT) - (SBV) edge [->,anchor=east] node {Compilation} (C99S); - \end{tikzpicture} - \caption{The new Copilot toolchain. } - \label{fig:New toolchain} - \end{figure} diff --git a/WC-End2End/flightTest.tex b/WC-End2End/flightTest.tex deleted file mode 100644 index d8083cf..0000000 --- a/WC-End2End/flightTest.tex +++ /dev/null @@ -1,4 +0,0 @@ -\section{Flight Test}~\label{sec:flighttest} - -Here we describe our flight tests. - diff --git a/WC-End2End/intro.tex b/WC-End2End/intro.tex deleted file mode 100644 index e9afc47..0000000 --- a/WC-End2End/intro.tex +++ /dev/null @@ -1,10 +0,0 @@ -\section{Introduction}\label{sec:intro} - -I've found it best to start with a general report document like this one to work in and then later customize it for a particular - confernece or journal. - - -The basic ideaa is to describe the end-to-end verification of our well clear monitor - starting with the mathematical/PVS. We would describe Copilot and the formulation of the well clear spec. We would then describe how we verify that the monitors do indeed satisfy the mathematical properties verifed in the PVS model. - -We would then describe how we synthesize assured monitors (C programs) from the Copilot spec. If space allows we would explain that when practical we would generate verified Machine code using CompCert. Giving us an end-to-end assurance argument. diff --git a/WC-End2End/paper.bib b/WC-End2End/paper.bib deleted file mode 100644 index 08f25ab..0000000 --- a/WC-End2End/paper.bib +++ /dev/null @@ -1,1847 +0,0 @@ - -% ================= -% Core background -%================== - -@INPROCEEDINGS{amast93, - AUTHOR={N. Halbwachs and F. Lagnier and P. Raymond}, - TITLE={Synchronous observers and the verification of reactive systems}, - BOOKTITLE={Third Int. Conf. on Algebraic Methodology and - Software Technology, AMAST'93}, - MONTH={June}, - EDITOR={M. Nivat and C. Rattray and T. Rus and G. Scollo}, - PUBLISHER={Springer Verlag}, - YEAR=1993 - } - -@InProceedings{safe, - author = {David Terei and Simon Marlow and Simon Peyton Jones and David Mazi\`{e}res}, - title = {Safe Haskell}, - OPTcrossref = {}, - OPTkey = {}, - booktitle = {Proceedings of the Haskell Symposium}, - OPTpages = {}, - year = {2012}, - OPTeditor = {}, - OPTvolume = {}, - OPTnumber = {}, - OPTseries = {}, - OPTaddress = {}, - OPTmonth = {}, - OPTorganization = {}, - Tpublisher = {ACM}, - OPTnote = {}, - OPTannote = {} -} - -@inproceedings{fof, - author = {Dagand, Pierre E. and Baumann, Andrew and Roscoe, Timothy}, - booktitle = {Proceedings of the Fifth Workshop on Programming Languages and Operating Systems (PLOS '09)}, - pages = {1--5}, - publisher = {ACM}, - title = {{Filet-o-Fish}: practical and dependable domain-specific languages for {OS} development}, - year = {2009} -} - -@Misc{ghc, - key = {GHC}, - author = {{GHC Team}}, - title = {The Glorious {G}lasgow {H}askell Compilation System User's Guide, Version 7.4.1}, - OPThowpublished = {}, - month = {March}, - year = {2012}, - note = {Available at \url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}}, - OPTannote = {} -} - -@inproceedings{typing, - author = {Baars, Arthur I. and Swierstra, S. Doaitse}, - title = {Typing dynamic typing}, - booktitle = {Intl. Conference on Functional Programming (ICFP)}, - month = {September}, - year = {2002}, - pages = {157--166}, - publisher = {ACM} -} - -@inproceedings{ocaml, - title = {Experience report: using {O}bjective {Caml} to develop safety-critical embedded tools in a certification framework}, - author = {Bruno Pagano and Olivier Andrieu and Thomas Moniot and Benjamin Canou and Emmanuel Chailloux and Philippe Wang and Pascal Manoury and Jean-Louis Colaço}, - year = {2009}, - pages = {215--220}, - booktitle = {International Conference on Functional Programming (ICFP)}, - editor = {Graham Hutton and Andrew P. Tolmach}, - publisher = {ACM} -} - -@inproceedings{appel, - author = {Andrew W. Appel}, - title = {Verified Software Toolchain}, - booktitle = {Programming Languages and Systems (ESOP)}, - year = {2011}, - pages = {1--17}, - series = {LNCS}, - volume = {6602}, - publisher = {Springer} -} - - - -@Proceedings{cli, - title = {Special Issue on System Verification: Journal of Automated Reasoning}, - year = {1989}, - OPTkey = {}, - OPTbooktitle = {}, - editor = {J Strother Moore}, - volume = {5}, - number = {4}, - OPTannote = {} -} - -@Article{turing, - author = {Len Sassaman and Meredith L. Patterson and Sergey Bratus and Anna Shubina}, - title = {The {H}alting Problems of Network Stack Insecurity}, - journal = {;login: The {USENIX} Magazine}, - year = {2011}, - OPTkey = {}, - volume = {36}, - number = {6}, - OPTpages = {}, - month = {December}, - OPTnote = {}, - OPTannote = {} -} - -@InProceedings{sampling, - author = {S. Fischmeister and Y. Ba}, - title = {Sampling-based Program Execution Monitoring}, - booktitle = {ACM International conference on Languages, compilers, and tools for embedded -systems ({LCTES})}, - pages = {133-142}, - year = {2010}, -} - -@InProceedings{borzoo, - author = {Borzoo Bonakdarpour and Samaneh Navabpour and Sebastian Fischmeister}, - title = {Sampling-based Runtime Verification}, - booktitle = {17th Intl. Symposium on Formal Methods (FM)}, - OPTpages = {}, - year = {2011}, -} - - - -@Misc{aeroperu, - OPTkey = {}, - author = {Peter B. Ladkin}, - title = {News and Comment on the {Aeroperu} B757 Accident; {AeroPeru} {F}light 603, 2 October 1996}, - OPThowpublished = {}, - OPTmonth = {}, - year = {2002}, - note = {Online article RVS-RR-96-16. Available at \url{http://www.rvs.uni-bielefeld.de/publications/Reports/aeroperu-news.html}}, - OPTannote = {} -} - -@article{ariane, - author = {Bashar Nuseibeh}, - title = {Soapbox: Ariane 5: Who Dunnit?}, - journal = {IEEE Software}, - volume = {14}, - number = {3}, - year = {1997}, - pages = {15--16} -} - -@inproceedings{gill, - author = {Andy Gill}, - title = {Type-Safe Observable Sharing in {H}askell}, - booktitle = {Proceedings of the 2009 {ACM} {SIGPLAN} {H}askell Symposium}, - year = {2009}, - month = {September} -} - - -@article{therac, -author = {Nancy G. Leveson and Clark S. Turner}, -title = {An Investigation of the {Therac-25} Accidents}, -journal ={Computer}, -volume = {26}, -year = {1993}, -pages = {18--41}, -publisher = {IEEE} -} - -@techreport{lustre-intro, -title = {Formal System Development with {L}ustre: Framework and Example}, -author = {Jan Mik\'{a}\^{c} and Paul Caspi}, -institution = {Verimag Technical Report}, -number = {TR-2005-11}, -year = {2005}, -OPTnote = {Available at \url{http://www-verimag.imag.fr/index.php?page=techrep-list&lang=en}} -} - - -@TECHREPORT{dutertre, - author = {Bruno Dutertre and Leonardo De Moura}, - title = {The {Y}ices {SMT} solver}, - institution = {SRI}, - year = {2006}, - notes = {Available at \url{http://yices.csl.sri.com/documentation.shtml}} -} - -@Misc{atom, - author = {Tom Hawkins}, - title = {Controlling Hybrid Vehicles with {H}askell}, - howpublished = {Presentation. \emph{Commercial Users of Functional Programming} (CUFP)}, - year = {2008}, - note = {Available at \url{http://cufp.galois.com/2008/schedule.html}.} -} - -@Misc{micromort, - author = {Ron Howard}, - title = {Life and Death Decisions}, - howpublished = {Presentation. \emph{Stategic Decision and Risk Management}, Stanford Certificate Program}, - month = {September}, - year = {2006}, - note = {Downloaded from \url{http://stanford-online.stanford.edu/sdrmda61w/session10b/slides/sld031.htm}.} -} - -@INPROCEEDINGS{rushbyss10, - AUTHOR = {John Rushby}, - TITLE = {Formalism in Safety Cases}, - BOOKTITLE = {Making Systems Safer: - Proceedings of the Eighteenth Safety-Critical Systems Symposium}, - YEAR = 2010, - EDITOR = {Chris Dale and Tom Anderson}, - PUBLISHER = {Springer}, - ADDRESS = {Bristol, UK}, - MONTH = feb, - PAGES = {3--17}, - NOTE = {Available at \url{http://www.csl.sri.com/users/rushby/papers/sss10.pdf}} -} - - -% Software and additional documentation available at \url{http://hackage.haskell.org/package/atom}.} -% } - -@inproceedings{scheduling, - author={Goossens, J. and Richard, P.}, - title={Overview of real-time scheduling problems (Invited Paper)}, - year={2004}, - booktitle={Euro Workshop on Project Management and Scheduling}, -} - %note ={Available at \url{http://www.lisi.ensma.fr/ftp/pub/documents/papers/2004/2004-EWPMSIP-Goossens.pdf}}, - -@inproceedings{rehger, - author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John}, - title = {Finding and understanding bugs in {C} compilers}, - booktitle = {Programming Language Design and Implementation (PLDI)}, - year = {2011}, - pages = {283--294}, - publisher = {ACM} -} - -@inproceedings{meijer, - author = {Leijen, Daan and Meijer, Erik}, - title = {Domain specific embedded compilers}, - booktitle = {Domain-Specific Languages Conference}, - year = {1999}, - publisher = {USENIX} -} - - -@Article{pareto, - author = {Reed, W. J}, - title = {The {P}areto, {Z}ipf and other power laws}, - journal = {Economics Letters}, - year = {2001}, - OPTkey = {}, - volume = {74}, - number = {1}, - pages = {15--19}, - OPTmonth = {}, - OPTnote = {}, - OPTannote = {} -} - - -@article{leroy, - author = {Leroy, Xavier}, - title = {Formal verification of a realistic compiler}, - journal = {Communications of the ACM}, - volume = {52}, - issue = {7}, - month = jul, - year = {2009}, - pages = {107--115} -} - - -@inproceedings{mcrypt, - author = {L. Pike and M. Shields and J. Matthews}, - title = {A verifying core for a cryptographic language compiler}, - booktitle = {Proceedings of the 6th Intl. Workshop on the ACL2 Theorem Prover and its Applications}, - year = {2006}, - pages = {1--10}, - publisher = {ACM}, -} -% note = {Available at \url{http://www.cs.indiana.edu/~lepike/pub_pages/acl2.html}} - -@article{lamport, - author = {Lamport, Leslie}, - title = {Time, clocks, and the ordering of events in a distributed system}, - journal = {Communications of the ACM}, - volume = {21}, - number = {7}, - year = {1978}, - pages = {558--565}, - publisher = {ACM} - } - -@inproceedings{copilot, - author = {Lee Pike and - Alwyn Goodloe and - Robin Morisset and - Sebastian Niller}, - title = {Copilot: A Hard Real-Time Runtime Monitor}, - booktitle = {Proceedings of the 1st Intl. Conf. on Runtime Verification (RV)}, - year = {2010}, - pages = {345-359}, - publisher = {Springer}, - volume = {6418} -} - -@Article{pike-isse-13, - author = {Lee Pike and Nis Wegmann and Sebastian Niller and Alwyn Goodloe}, - title = {Copilot: Monitoring Embedded Systems}, - journal = {Innovations in Systems and Software Engineering}, - year = {2013}, - volume = {9}, - number = {4} -} - -@InProceedings{pike-icfp-12, - author = {Lee Pike and Nis Wegmann and Sebastian Niller and Alwyn Goodloe}, - title = {Experience Report: a Do-It-Yourself High-Assurance Compiler}, - booktitle = {Proceedings of the Intl. Conference on Functional Programming (ICFP)}, - publisher = {ACM}, - year = {2012}, - month = {September} -} - -@InProceedings{assuring-guardians, - author = {Jonathan Laurent and Alwyn Goodloe and Lee Pike}, - title = {Assuring the Guardians}, - booktitle = {Proceedings of the 6th Intl. Conf. on Runtime Verification (RV)}, - year = {2015}, - xvolume = {9333}, - xseries = {Lecture Notes in Computer Science}, - xpages = {87--101}, - xpublisher = {Springer International Publishing} -} - -@article{javamop, - author = {Chen, Feng and d'Amorim, Marcelo and Ro\c{s}u, Grigore}, - title = {Checking and Correcting Behaviors of Java Programs at Runtime with {Java-MOP}}, - journal = {Electronic Notes in Theoretical Computer Science}, - volume = {144}, - issue = {4}, - month = {May}, - year = {2006}, - pages = {3--20}, - publisher = {Elsevier} -} - -@incollection {controller, - author = {Asarin, Eugene and Maler, Oded and Pnueli, Amir}, - title = {Symbolic controller synthesis for discrete and timed systems}, - booktitle = {Hybrid Systems II}, - series = {LNCS}, - publisher = {Springer}, - pages = {1-20}, - volume = {999}, - year = {1995} -} - - - -@PhdThesis{bauer, - author = {Andreas Klaus Bauer}, - title = {Model-based runtime analysis of distributed reactive systems}, - school = {Institut f\"{u}r Informatik der Technischen Universit\"{a}t M\"{u}nchen}, - year = {2006}, - OPTkey = {}, - OPTtype = {}, - OPTaddress = {}, - OPTmonth = {}, - OPTnote = {Available at \url{http://deposit.ddb.de/cgi-bin/dokserv?idn=985347074&dok_var=d1&dok_ext=pdf&filename=985347074.pdf}}, - OPTannote = {} -} - -@inproceedings{syncraft, - author = {Bonakdarpour, Borzoo and Kulkarni, Sandeep S.}, - title = {{SYCRAFT}: A Tool for Synthesizing Distributed Fault-Tolerant Programs}, - booktitle = {International Conference on Concurrency Theory (CONCUR '08)}, - year = {2008}, - pages = {167--171}, - publisher = {Springer} -} - -@inproceedings{sandeep, - author = {Bonakdarpour, Borzoo and Kulkarni, Sandeep S}, - title = {Incremental synthesis of fault-tolerant real-time programs}, - booktitle = {Proceedings of the 8th international conference on stabilization, safety, and security of distributed systems (SSS'06)}, - year = {2006}, - pages = {122--136}, - numpages = {15}, - publisher = {Springer-Verlag} -} - -@TechReport{rushby-possibly, - author = {Bev Littlewood and John Rushby}, - title = {Reasoning about the Reliability Of Diverse Two-Channel Systems In which One Channel is "Possibly Perfect"}, - institution = {SRI}, - year = {2010}, - OPTkey = {}, - type = {Technical Report}, - number = {SRI-CSL-09-02}, - OPTaddress = {}, - month = {January}, - OPTnote = {Available at \url{http://www.csl.sri.com/users/rushby/abstracts/csl-09-02}}, - OPTannote = {} -} - -@Misc{DO178B, - author = {RTCA}, - howpublished = {RTCA, Inc.}, - title = {Software Considerations in Airborne Systems and Equipment Certification}, - note = {RCTA/DO-178B}, - year = {1992} - } - -@Misc{DO254, - key = {RTCA}, - howpublished = {RTCA, Inc.}, - title = {Design Assurance Guidelines for Airborne Electronic Hardware}, - note = {{RCTA/DO254}}, - year = {2000} - } - -@techreport{bigfaa, - AUTHOR = {John Rushby}, - TITLE = {Formal Methods and Digital Systems Validation for Airborne Systems}, - INSTITUTION = {{NASA}}, - YEAR = {1993}, - NUMBER = {CR--4551}, - MONTH = {{December}} -} - - - -@Book{MannaP, - author = {Z. Manna and A. Pnueli}, - title = {The Temporal Logic of Reactive and Concurrent Systems}, - publisher = {Springer Verlag}, - year = {1992} -} - - -% ==================== -% Esterel -% ==================== - - -@Article{BerryG92, - author = {G. Berry and G. Gonthier}, - title = {The Eserel Synchronous Programming Language: Design, Semantics, and Implementation}, - journal = {The Science of Computer Programming}, - year = {1992}, - volume = {19}, - number = {2}, - pages = {87--152} -} - -% ===================== -% Lustre -% ===================== - - - -@Misc{LustreComp, - OPTkey = {}, - OPTauthor = {}, - OPTtitle = {Lustre V6 Compiler}, - OPThowpublished = {}, - OPTmonth = {}, - OPTyear = {}, - OPTnote = {http://www-verimag.imag.fr/Lustre-V6.html}, - OPTannote = {} -} - -@Article{BenvenisteCHGS02, - author = {A. Benveniste and P. Caspi and S. Edwards and N. Halbwachs and P. Le~Guernic and R. de~Simone}, - title = {The Synchronous Languages Twelve Years Later}, - journal = {Proceedings of the IEEE}, - year = {2002}, - volume = {91}, - number = {1}, - pages = {64--83} -} - -@InProceedings{CaspiPHP87, - author = {P. Caspi and D. Pialiud and N. Halbwachs and J. Plaice}, - title = {{LUSTRE}: a Declarative Language for Programming Synchronous Systems}, - booktitle = {14th Symposium on Principles of Programming Languages}, - pages = {178-188}, - year = {1987} -} - - - @InProceedings{HalbwachsRR991, - author = {N.Halbwachs and P Raymond and C. Ratel}, - title = {Generating Efficient Code from Data-Flow Programs}, - booktitle = {Third International Symposium on Programming Language Implementation and Logic Programming }, - OPTpages = {}, - year = {1991} -} - - -@INPROCEEDINGS{Halbwachs93, - author = {N. Halbwachs and F. Lagnier and P. Raymond}, - title = {Synchronous Observers and the Verification of Reactive Systems}, - booktitle = {Third International Conference on Algebraic Methodology and Software Technology}, - year = {1993}, - pages = {83--96}, - publisher = {Springer Verlag} -} - - - -General Overview -%-------------------------------------------------------- - -@INBOOK{ColinM05, -AUTHOR = {Severine Colin and Leonardo Mariani}, -TITLE = {Model-based Testing of Reactive Systems}, -CHAPTER = {Run-time Verification}, -pages = {525-556}, -PUBLISHER = {Springer Verlag}, -YEAR = {2005}, -volume = {3472}, -series = {LNCS}, -} -%editor = {Manfred Broy and Bengt Jonsson and Joost-Pieter Katoen and Martin Leucker and Alexander Pretschner}, - - - -@Article{DelgadoGR04, - author = {N. Delgado and A. Gates and S. Roach}, - title = {A Taxonomy and Catalog of Runtime Monitoring Tools}, - journal = {IEEE Transactions of Software Engineering}, - year = {2004}, - volume = {30}, - number = {12}, - pages = {859--872} -} - -@Article{Schroeder95, - author = {B. Schroeder}, - title = {On-Line Monitoring: A Tutorial}, - journal = {IEEE Computer}, - year = {1995}, - volume = {28}, - number = {6}, - pages = {72--78} -} - - -%------------------------- -% Penn work on MAC -%------------------------- - - -@InProceedings{KimVBKLS99, - author = {M. Kim and M. Viswanathan and H. Ben-Abdallah and S. Kannan and I. Lee - and O. Sokolsky}, - title = {Formally specified monitoring of temporal properties}, - booktitle = {11th Euromicro Conference on Real-Time Systems}, - pages = {114--122}, - year = {1999}, - } - -@InProceedings{LeeKSV99, - author = {M. Kim and O. Sokolsky and M. Viswanathan}, - title = {Runtime assurance based on formal specifications}, - booktitle = {International Conference - on Parallel and Distributed Processing Techniques and Applications}, - pages = {279--287}, - year = {1999} - } - - -@Article{KimLKS04, - author = { M. Kim and I. Lee and S. Kannan and O. Sokolsky}, - title = {{Java-MaC}: a Run-time Assurance Tool for {J}ava}, - journal = {Formal Methods in System Design}, - year = {2004}, - volume = {24}, - number = {1}, - pages = {129--155} -} - - -@InProceedings{KimLSSS02, - author = {M. Kim and I. Lee and U. Sammapun and J. Shin and O. Sokolsky}, - title = {Monitoring, Checking, and Steering of Real-Time Systems}, - series = {ENTCS}, - year = {2002}, - volume = {70}, - number = {4}, - booktitle = {Proceedings of the 2nd Intl. Conf. on Runtime Verification} -} - -@Article{SokolskySLK05, - author = {O. Sokolsky and U. Sammapun and I. Lee and J. Kim}, - title = {Run-Time Checking of Dynamic Properties}, - series = {ENTCS}, - year = {2005}, - volume = {144}, - number = {4}, - pages = {91--108}, - booktitle = {Proceedings of the 5th Intl. Conf. on Runtime Verification} - } - - - -@Misc{cmac, - author = {O. Sokolsky}, - title = {{C MaC}}, - howpublished = {Available from University of Pennsylvania Real-Time Systems Gorup}, - note = {\url{rtg.cis.upenn.edu}} - -} - -%-------------------------------------------------------------------- -% Rosu general and MOP -%------------------------------------------------------------------- - -@inproceedings{havelundc, - author = {Klaus Havelund}, - title = {Runtime Verification of {C} Programs}, - booktitle = {Testing of Software and Communicating Systems (TestCom/FATES)}, - year = {2008}, - publisher = {Springer}, - pages = {7--22} -} - -@Article{HavelundR04A, - author = {K. Havelund and G. Ro\c{s}u}, - title = {An Overview of the Runtime Verification Tool {J}ava {P}ath{E}xplorer}, - journal = {Formal Methods in System Design}, - year = {2004}, - volume = {24}, - number = {2}, - pages = {189--215} -} - -@Article{HavelundR04B, - author = {K. Havelund and G. Ro\c{s}u}, - title = {Efficient Monitoring of Safety Properties}, - journal = {International Journal on Software Tools for Technology Transfer }, - year = {2004}, - volume = {6}, - number = {2}, - Tpages = {158--173} -} - - - -@inproceedings{ChenR05, -author={F. Chen and G. Ro\c{s}u}, -title={{Java-MOP:} A Monitoring Oriented Programming Environment for {Java}}, -booktitle={11th Intl. Conf. on Tools and Algorithms for the construction and analysis of systems ({TACAS'05})}, -publisher={Springer}, -series={LNCS}, -volume={3440}, -pages= {546-550}, -year={2005} -} - - -@Misc{framac, - key = {Frama-C webpage}, - OPTauthor = {{CEA~LIST} and {INRIA-Saclay} (developin}, - title = {{Frama-C}}, - OPThowpublished = {Webpage}, - OPTmonth = {}, - OPTyear = {Accessed 2010}, - note = {Accessed August, 2010. \url{http://frama-c.com/index.html}}, - OPTannote = {} -} - -@InProceedings{ChenAR04, - author = {F. Chen and M. D'Amorim and G. Ro\c{s}u}, - title = {A Formal Monitoring-Base Framewrok for Software Development Analysis}, - booktitle = {Proceedings of the 6th International Conference on Formal Engineering Methods (ICFEM'04)}, - pages = {357--373}, - year = {2004}, - OPTnumber = {3308}, - series = {LNCS}, - publisher = {Springer} - } - - -@InProceedings{ChenR07, - author = {F. Chen and G. Ro\c{s}u}, - title = {{MOP:} An Efficient and Generic Runtime Verification Framework}, - booktitle = {Object Oriented Programming, Systems, Languages, and Applications}, - pages = {569--588}, - year = {2007} -} - -%------------------------------------------------------- -% Rosu Generating Monitors -%------------------------------------------------------- -@InProceedings{HavelundR02, - author = {K. Havelund and G. Ro\c{s}u}, - title = {Synthesizing Monitors for Safety Properties}, - booktitle = {Tools and Algorithms for Construction and Analysis of Systems}, - pages = {342-356}, - year = {2002} -} - - - -@InProceedings{RosuCB08, - author = {G. Rosu and F. Chen and T. Ball}, - title = {Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns}, - booktitle = {{RV}'08: Proceedings of Runtime Verification}, - year = {2008}, - note = {To Appear}, - -} - -%------------------------------------------------------- -% Rosu Distributed. -%------------------------------------------------------- - - -@InProceedings{SenVAR04, - author = {K. Sen and A. Vardhan and G. Agha and G. Rosu}, - title = {Efficient Decentralized Monitoring of Safety in Distributed Systems}, - booktitle = {{ICSE}'04: Proceedings of 6th International Conference on Software Engineering}, - pages = {418--427}, - year = {2004} -} - - - - -% ------------------------------------ -% RT -%------------------------------------- - -@InProceedings{PellizzoniCR08A, - author = {R. Pellizzoni and P. Meredith and M. Caccamo and G. Rosu }, - title = {Hardware Runtime Monitoring for Dependable COTS-based -Real-Time Embedded Systems}, - booktitle = {{RTSS}'08: Proceedings of the 29th IEEE Real-Time System Symposium}, - pages = {481--491}, - year = {2008} -} - -@inproceedings{PellizzoniCR08B, - author = {Pellizzoni,, Rodolfo and Meredith,, Patrick and Caccamo,, Marco and Ro\c{s}u,, Grigore}, - title = {Hardware Runtime Monitoring for Dependable {COTS}-Based Real-Time Embedded Systems}, - booktitle = {RTSS '08: Proceedings of the 2008 Real-Time Systems Symposium}, - year = {2008}, -pages = {481--491}, -publisher = {IEEE Computer Society}, - address = {Washington, DC, USA}, - } - - - -%--------------------- -% -%--------------------- - -@INPROCEEDINGS{Rushby09:SEFM, - AUTHOR = {John Rushby}, - TITLE = {Software Verification and System Assurance}, - BOOKTITLE = {Intl. Conf. on Software Engineering and Formal Methods ({SEFM})}, - OPTEDITOR = {Dang Van Hung and Padmanabhan Krishnan}, - OPTADDRESS = {Hanoi, Vietnam}, - ORGANIZATION = {IEEE}, - PAGES = {3--10}, - MONTH = nov, - YEAR = 2009 -} - - - -@InProceedings{BarringerGHS04, - author = {H. Barringer and A. Goldberg and K. Havelund and K. Sen}, - title = {Rule-Based Runtime Verification}, - booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)}, - year = {2004}, - series = {LNCS}, - number = {2937}, - publisher = {Springer-Verlag} - } - -@InProceedings{BarringerRH07, - author = {H. Barringer and D. Rydeheard and K. Havelund}, - title = {Rule systems for run-time monitoring: From Eagle to Ruler}, - booktitle = { {RV}07: Proceedings of Runtime Verification 2007}, - pages = {111--125}, - year = {2007}, - number = {4839}, - series = {LNCS}, - publisher = {Springer-Verlag} -} - - - -%======================= -% Monitoring C programs -% ====================== -@InProceedings{Havelund08, - author = {K. Havelund}, - title = {Runtime Verification of {C} Programs}, - booktitle = {{T}est{C}om/{FATES}}, - OPTpages = {}, - year = {2008}, - number = {5047}, - series = {LNCS}, - publisher = {Springer-Verlag} -} - - ---------------------- -% Real-Time -% ------------------------------------ -@inproceedings{SavorS97, - author = {T. Savor and R. Seviora}, - title = {An Approach to Automatic Detection of Software Failures in Real-Time Systems}, - booktitle = {IEEE Real-Time Technology and Applications Symposium}, - pages = {136--147}, - year = {1997} - } - -@inproceedings{mokL97, - author = {A. Mok and G. Liu}, - title = {Efficient Run-Time Monitoring of Timing Constraints}, - booktitle = {IEEE Real-Time Technology and Applications Symposium}, - pages = {252--262}, - year = {1997} - } - - - -%------------------------- -% Monitoring metric and other temporal logics -% ------------------------ - - -@InProceedings{AlurH90, - author = {R. Alur and T. Henzinger}, - title = {Real time logics: complexity and expressiveness}, - booktitle = {Fifth Annual Symposium on Logic in Computer Science}, - pages = {390-401}, - year = {1990}, - publisher = {IEEE Computer Society Press} -} - - - -@InProceedings{AlurH92, - author = {R. Alur and T. Henzinger}, - title = {Logics and Models of Real Time: A Survey}, - booktitle = {Real Time Theory and Practice}, - OPTpages = {}, - year = {1992}, - volume = {LNCS}, - publisher = {Springer-Verlag} - -} - -@InProceedings{BasinKMP08, - author = {D. Basin and F. Klaedtke and S. Muller and B. Pfitzmann}, - title = {Runtime Monitoring of Metric First-Order Temporal Properties}, - booktitle = {Foundations of Software Technology and Theoretical Computer Science}, - pages = {49--60}, - year = {2008}, - editor = {R. Hariharan and M. Mukund and V. Vinay}, - series = {Leibniz International Proceedings in Informatics}, - publisher = {Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany.} - -} - -@Article{simplex, - author = {Lui Sha}, - title = {Using Simplicity to Control Complexity}, - journal = {IEEE Software}, - month = {July/August}, - year = {2001}, - publisher = {IEEE}, - pages = {20--28}, -} - -@Article{Drusinky06, - author = {D, Drusinsky}, - title = {On-line Monitoring of Metric Temporal Logic wit Time-Series Constraints Using Alternating Finite Automata}, - journal = {Journal of Universal Computer Science}, - year = {2006}, - volume = {12}, - number = {5}, - pages = {482--498} - -} - - - -@Article{ThatiR05, - author = {P. Thati and G. Ro\c{s}u}, - title = {Monitoring Algorithms for Metric Temporal Logic Specifications}, - journal = {Electronic Notes Theoretical Computer Science}, - year = {2004}, - volume = {113} -} - -@InProceedings{MalerNP05, - author = {O. Maler and D. Nickovic and A. Pnueli}, - title = {Real Time Temporal Logic: Past, Present, Future}, - booktitle = {Formal Modeling and Analysis of Timed Systems}, - pages = {2--16}, - year = {2005}, - volume = {LNCS}, - publisher = {Springer-Verlag} - -} - - -@InProceedings{ColomboPS09, - author = {C. Colombo and G. Pace and G. Schneider}, - title = {Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties}, - Tbooktitle = {Runtime Verification 2009}, - pages = {135--149}, - year = {2009}, - volume = {LNCS}, - publisher = {Springer-Verlag} - -} - - - - -% ========= -% LOLA paper -%============ -@InProceedings{lola, - - author = {B. D'Angelo and S. Sankaranarayanan and C. Sánchez and W. Robinson and Zohar Manna - and B. Finkbeiner and H. Spima and S. Mehrotra}, - title = {{LOLA}: Runtime Monitoring of Synchronous Systems}, - booktitle = {12th International Symposium on Temporal Representation and Reasoning}, - pages = {166-174}, - year = {2005}, - publisher = {IEEE} - -} -% ==================== -%This si duplicated. Replace reference w/ existing reference. -% ==================== - -@article{ptltl, - author = {Havelund, Klaus and Ro\c{s}u, Grigore}, - title = {Efficient monitoring of safety properties}, - journal = {Int. J. Softw. Tools Technol. Transf.}, - volume = {6}, - number = {2}, - year = {2004}, - issn = {1433-2779}, - pages = {158--173}, - doi = {http://dx.doi.org/10.1007/s10009-003-0117-6}, - publisher = {Springer-Verlag}, - address = {Berlin, Heidelberg}, - } - - - - -@Misc{pitot, - key = {Aviation}, - author = {{Aviation Today}}, - title = {More Pitot Tube Incidents Revealed}, - howpublished = {Aviation Today}, - month = {February}, - year = {2011}, - note = {Available at \url{http://www.aviationtoday.com/regions/usa/More-Pitot-Tube-Incidents-Revealed_72414.html}}, - OPTannote = {} -} - -@Misc{RTJava, - OPTkey = {}, - author = {TimeSys Corporation}, - title = {JSR-000282 Real-Time Specification for {J}ava 1.1}, - OPThowpublished = {}, - OPTmonth = {}, - OPTyear = {}, - OPTnote = {}, - OPTannote = {} -} - -% ---------------------------------- -% -% ---------------------------------- - -@InProceedings{SammapunLS05, - author = {U. Sammapun and I. Lee and O. Sokolsky}, - title = {{RT-MaC:} Runtime Monitoring and Checking of Quantitative and Probabilistic Properties}, - booktitle = {11th IEEE Intl. Conf. on Embedded and Real-Time Computing Systems and Applications}, - pages = {147--153}, - year = {2005} -} - - -@Misc{ATSB07, - key = {ATSB}, - author = {{Australian Transport Safety Bureau}}, - title = {In-Flight Upset Event 240{Km} {N}orth-{W}est of {P}erth, {WA} {B}oeing {C}ompany 777-200, 9{M-MRG} 1 {A}ugust 2005}, - publisher = {Australian Transport Safety Bureau}, - howpublished = {ATSB Transport Safety Investigation Report}, - year = {2007}, - OPTnote = {Aviation Occurrace Report - 200503722} -} - -@Misc{ATSB08, - author = {Kerryn Macaulay}, - title = {{ATSB} Preliminary Factual Report, In-Flight Upset, {Q}antas {A}irbus {A330}, - 154 {K}m {W}est of {L}earmonth, {WA}, 7 {O}ctober 2008}, - howpublished = {Australian Transport Safety Bureau Media Release }, - month = {{November 14}}, - year = {2008}, - note = {Available at \url{http://www.atsb.gov.au/newsroom/2008/release/2008_45.aspx}} - } - -@Misc{ATSB08A, - key = {ATSB}, - author = {{Australian Government}}, - title = {In-Flight Upset 154 {K}m {W}est of {L}earmonth 7 {O}ctober 2008 {VH-QPA} {A}irbus {A330-303}}, - howpublished = {Australian Transport Safety Bureau Aviation Occurrence Investigation AO-2008-70}, - OPTmonth = {}, - note = {Available at \url{http://www.atsb.gov.au/publications/investigation_reports/2008/AAIR/aair200806143.aspx}}, - year = "2008" -} - -@Article{BhargavanCMG01, - author = {K. Bhargavan and S. Chandra and P. McCann and C.A. Gunter}, - title = {What Packets May Come: Automata for Network Monitoring}, - journal = {SIGPLAN Notices}, - year = {2001}, - volume = {35}, - number = {3}, - pages = {209--219} -} - -@inproceedings{mats, - author = "Gao, Jimin and Heimdahl, Mats and Van Wyk, Eric", - title = "Flexible and Extensible Notations for Modeling Languages", - booktitle = "Fundamental Approaches to Software Engineering (FASE)", - series = "LNCS", - publisher = "Springer Verlag", - volume = 4422, - pages = "102--116", - month = "March", - year = 2007 -} - -@INPROCEEDINGS{qc, - author = {Koen Claessen and John Hughes}, - title = {{QuickCheck}: A Lightweight Tool for Random Testing of {H}askell Programs}, - booktitle = {ACM SIGPLAN Notices}, - year = {2000}, - pages = {268--279}, - publisher = {ACM} -} - -@inproceedings{lustre, -author = {N. Halbwachs and P. Raymond}, -title = {Validation of Synchronous Reactive Systems: from Formal Verification to Automatic Testing}, -booktitle = {ASIAN'99, Asian Computing Science Conference}, -publisher={LNCS 1742, Springer}, -year = {1999}, -month = {December} -} - -@Article{BhargavanG02, - author = { K. Bhargavan and C. A. Gunter}, - title = {Requirement for a Practical Network Event Recognation Language}, - journal = {Electronic Notes in Theoretical Computer Science}, - year = {2002}, - volume = {70}, - number = {4}, - pages = {1--20} -} - -@Misc{mdm08, - author = {Chris Bergin}, - title = "Faulty {MDM} Removed", - note = {Available at \url{http://www.nasaspaceflight.com/2008/05/sts-124-frr-debate-outstanding-issues-faulty-mdm-removed/}.}, - howpublished = {{NASA Spaceflight.com}}, - month = {{M}ay 18}, - year = {2008} - } - - -@Misc{mdm08A, - author = {Chris Bergin}, - title = "{STS}-126: Super Smooth Endeavor Easing Through the Countdown to {L}-1", - note = {Available at \url{http://www.nasaspaceflight.com/2008/11/sts-126-endeavour-easing-through-countdown/}. (Downloaded {Feb} 3, 2009)}, - howpublished = {{NASA} Spaceflight.com}, - month = {{November 13}}, - year = {2008} - } - -@inproceedings{mjrty, - author = {Robert S. Boyer and - J. Strother Moore}, - title = {{MJRTY}: A Fast Majority Vote Algorithm}, - booktitle = {Automated Reasoning: Essays in Honor of Woody Bledsoe}, - year = {1991}, - pages = {105-118} -} - -@INPROCEEDINGS{Rushby01:buscompare, - AUTHOR = {John Rushby}, - TITLE = {Bus Architectures For Safety-Critical Embedded Systems}, - BOOKTITLE = {Workshop on Embedded Software ({EMSOFT})}, - YEAR = 2001, - OPTEDITOR = {Tom Henzinger and Christoph Kirsch}, - PUBLISHER = {Springer}, - OPTADDRESS = {Lake Tahoe, CA}, - MONTH = {October}, - SERIES = {LNCS}, - OPTVOLUME = 2211, - PAGES = {306--323} -} - -@inproceedings{Tha88:RDSS, - author = {Philip M. Thambidurai and - You-Keun Park}, - title = {Interactive Consistency with Multiple Failure Modes}, - booktitle = {Proceedings of the Seventh Symposium on Reliable Distributed Systems}, - year = {1988}, - pages = {93--100} -} - -@ARTICLE{ssa, - author = {Ron Cytron and Jeanne Ferrante and Barry K. Rosen and Mark N. Wegman and F. Kenneth Zadeck}, - title = {Efficiently computing static single assignment form and the control dependence graph}, - journal = {ACM Transactions on Programming Languages and Systems}, - year = {1991}, - volume = {13}, - pages = {451--490} -} - - -@inproceedings{latron, - author = {Latronico, Elizabeth}, - title = {Design Time Reliability Analysis of Distributed Fault Tolerance Algorithms}, - booktitle = {Proceedings of the 2005 International Conference on Dependable Systems and Networks}, - year = {2005}, - pages = {486--495}, - publisher = {IEEE} -} - -@InProceedings{pike-rv-11, - author = {Lee Pike and Sebastian Niller and Nis Wegmann}, - title = {Runtime Verification for Ultra-Critical Systems}, - booktitle = {Proceedings of the 2nd Intl. Conference on Runtime Verification}, - publisher = {Springer}, - series = {LNCS}, - year = {2011}, - month = {September} -} - - -@TechReport{monitors, - author = {Alwyn Goodloe and Lee Pike}, - title = {Monitoring Distributed Real-Time Systems: A Survey and Future Directions}, - institution = {NASA Langley Research Center}, - year = {2010}, - number = {NASA/CR-2010-216724}, - month = {July}, - OPTnote = {Available at \url{http://ntrs.nasa.gov/search.jsp?R=278742&id=3&as=false&or=false&qs=Ns%3DArchiveName%257c0%26N%3D4294643047}} -} - -@inproceedings{sheeran, - author = {Mary Sheeran and - Satnam Singh and - Gunnar St{\aa}lmarck}, - title = {Checking Safety Properties Using Induction and a SAT-Solver}, - booktitle = {Formal Methods in Computer-Aided Design (FMCAD)}, - year = {2000}, - pages = {108--125}, - series = {LNCS}, - volume = {1954}, - publisher = {Springer} -} - -@inproceedings{feldspar1, - author = {Emil Axelsson and - Koen Claessen and - Mary Sheeran and - Josef Svenningsson and - David Engdal and - Anders Persson}, - title = {The Design and Implementation of {F}eldspar - An Embedded - Language for Digital Signal Processing}, - booktitle = {Implementation and Application of Functional Languages}, - year = {2011}, - publisher = {Springer}, - series = {LNCS}, - volume = {6647}, - pages = {121--136} -} - - -@inproceedings{tinelli, - author = {Temesghen Kahsai and Yeting Ge and Cesare Tinelli}, - title = {Instantiation-Based Invariant Discovery}, - booktitle = {3rd NASA Formal Methods Symposium}, - OPTEditor = {M. Bobaru and K. Havelundand G. Holzmann and R. Joshi}, - publisher = {Springer}, - pages = {192--207}, - series = {LNCS}, - volume = {6617}, - year = {2011} -} - -@inproceedings{gadts, - author = {Schrijvers, Tom and Peyton Jones, Simon and Sulzmann, Martin and Vytiniotis, Dimitrios}, - title = {Complete and decidable type inference for {GADT}s}, - booktitle = {International Conference on Functional Programming (ICFP)}, - series = {ICFP '09}, - year = {2009}, - pages = {341--352}, - publisher = {ACM} -} - -@ARTICLE{blast, - author = {Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar}, - title = {The software model checker {BLAST}: Applications to software engineering}, - journal = {International Journal on Software Tools for Technology Transfer}, - year = {2007} -} - -@inproceedings{cbmc, - AUTHOR = { Clarke, Edmund - and Kroening, Daniel - and Lerda, Flavio }, - TITLE = { A Tool for Checking {ANSI-C} Programs }, - BOOKTITLE = { Tools and Algorithms for the Construction and Analysis of Systems (TACAS) }, - YEAR = { 2004 }, - PUBLISHER = { Springer }, - PAGES = { 168--176 }, - SERIES = { LNCS }, - OPTVOLUME = { 2988 } -} - -@InProceedings{rvRushby, - author = {John Rushby}, - title = {Runtime Certification}, - OPTcrossref = {}, - OPTkey = {}, - booktitle = {Eighth Workshop on Runtime Verification (RV08)}, - pages = {21--35}, - year = {2008}, - OPTeditor = {}, - volume = {5289}, - OPTnumber = {}, - series = {LNCS} -} - -% ---------------------------------- -% -% --------------------------------- -@Book{lynch, - author = {Nancy A. Lynch}, - ALTeditor = {}, - title = {Distributed Algorithms}, - publisher = {Morgan Kaufmann}, - year = {1996} -} - -@Article{lamport95byzantine, - author = {L. Lamport and R. Shostak and M. Pease}, - title = {The {Byzantine} Generals Problem}, - journal = {ACM Transactions on Programming Languages and Systems}, - year = {1982}, - OPTkey = {}, - volume = {4}, - Tnumber = {3}, - pages = {382--401}, - month = {July}, - OPTnote = {}, - OPTannote = {}, - Optnote = {Available at \url{http://citeseer.nj.nec.com/lamport82byzantine.html}} -} - -@InProceedings{laprie, - author = {Jean-Claude Laprie}, - title = {Dependability---Its Attributes, Impairments and Means}, - OPTcrossref = {}, - OPTkey = {}, - booktitle = {Predictability Dependable Computing Systems}, - pages = {3--24}, - year = {1995}, - OPTeditor = {B. Randell and J.-C. Laprie and H. Kopetz and B. Littlewood}, - OPTvolume = {}, - OPTnumber = {}, - OPTseries = {{ESPRIT} Basic Research Series}, - OPTaddress = {}, - OPTmonth = {}, - OPTorganization = {}, - publisher = {Springer}, - OPTnote = {}, - OPTannote = {} -} - - -@article{butler, - author = {Butler, R. W. and Finelli, G. B.}, - title = {The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software}, - journal = {IEEE Transactions on Software Engineering}, - volume = {19}, - issue = {1}, - month = {January}, - year = {1993}, - pages = {3--12}, - publisher = {IEEE Press} -} - -@inproceedings{msc, - author = {Kr\"{u}ger, Ingolf H. and Meisinger, Michael and Menarini, Massimiliano}, - title = {Runtime verification of interactions: from {MSCs} to aspects}, - booktitle = {International Conference on Runtime Verification}, - year = {2007}, - pages = {63--74}, - publisher = {Springer} -} - -@article{l4, - author = {Gerwin Klein - and June Andronick - and Kevin Elphinstone - and Gernot Heiser - and David Cock - and Philip Derrin - and Dhammika Elkaduwe - and Kai Engelhardt - and Rafal Kolanski - and Michael Norrish - and Thomas Sewell - and Harvey Tuch - and Simon Winwood}, - title = {{seL4}: Formal Verification of an {OS} Kernel}, - journal = {Communications of the ACM (CACM)}, - publisher = {ACM}, - year = {2010}, - month = jun, - pages = {107--115}, - volume = 53, - number = 6 -} - - - -%------------------------ -% Time Triggered -% ------------------------ - - - -@Book{kopetz, - author = {Hermann Kopetz}, - ALTeditor = {}, - title = {Real-Time Systems}, - publisher = {Kluwer Academic Publishers}, - year = {1997}, - series = {The Kluwer International Series in Engineering and Computer Science} - -} - - - -@inproceedings{ttethernet, - author = {Kopetz,, Hermann}, - title = {The Rationale for Time-Triggered Ethernet}, - booktitle = {Real-Time Systems Symposium (RTSS)}, - year = {2008}, - pages = {3--11}, - publisher = {IEEE} - } - - -%--------- -@book{Haskell98, - editor = {Simon Peyton Jones}, - howpublished = {PDF}, - pages = 277, - publisher = {http://haskell.org/}, - title = {{H}askell 98 Language and Libraries: The Revised Report}, - type = {Language Definition}, - year = 2002 -} -% url = {http://haskell.org/definition/haskell98-report.pdf}, - -@InProceedings{FriedmanW76, - author = {D. Friedman and D. Wise}, - title = {{CONS Should Not Evaluate its Argument}}, - booktitle = {Automata, Languages and Programming}, - pages = {256--284}, - year = {1976}, - publisher = {University of Edinburgh Press} -} - -% ------- -@techreport{ISO:C99, - author = {ISO}, - editor = {WG14}, - note = {ISO/IEC 9899:1999 draft}, - title = {{ISO C} Standard}, - url = {http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1124.pdf}, - year = 1999, -} - -@inproceedings{driscoll, - author = {K. Driscoll and - B. Hall and - H{\aa}kan Sivencrona and - P. Zumsteg}, - booktitle = {Computer Safety, Reliability, and Security, 22nd International - Conference, {SAFECOMP}}, - title = {Byzantine Fault Tolerance, from Theory to Reality}, - year = {2003}, - pages = {235-248}, - publisher = {Springer} -} - - -@INPROCEEDINGS{qc1, - author = {Koen Claessen and John Hughes}, - title = {Testing Monadic Code with {QuickCheck}}, - booktitle = {In Proc. ACM SIGPLAN workshop on Haskell}, - year = {2002}, - pages = {65--77} -} - -@phdthesis{miner, - author = {Miner, Paul}, - note = {Adviser-Johnson, Steven D.}, - title = {Hardware verification using coinductive assertions}, - year = {1998}, - school = {Indiana University, Bloomington} - } - -% publisher = {Indiana University, Bloomington} - - -@InProceedings{DwyerDE08, - author = {M.B. Dwyer and M. Diep and S. Elbaum}, - title = {Reducing the Cost of Path Property Monitoring Through Sampling}, - booktitle = {Proceedings of the 23rd International Conference on Automated Software Engineering}, - pages = {228--237}, - year = {2008} -} - - -@article{LennartMS08, - author = {L. Augustsson and H. Mansell and G. Sittampalam}, - title = {{Paradise:} a two-stage {DSL} embedded in {H}askell}, - journal = {SIGPLAN Not.}, - volume = {43}, - number = {9}, - year = {2008}, - issn = {0362-1340}, - pages = {225--228}, - publisher = {ACM}, - address = {New York, NY, USA}, - } - - - -@Misc{scade, - author = {Esterel Technologies}, - OPTtitle = {}, - note = {\url{http://www.esterel-technologies.com/technology/success-stories/airbus}} - -} - - - - -@InProceedings{SammapunLS0R7, - author = {U. Sammapun and I. Lee and O. Sokolsky and J. Regehr}, - title = {Statistical Runtime Checking of Probabilistic Properties}, - booktitle = {{RV'07}: Proceedings of Runtime Verification}, - pages = {164--175}, - year = {2007}, - series = {LNCS} -} - - - - -%--------------- -@InProceedings{FishmeisterL09, - author = {S. Fishmeister and P. Lam}, - title = {On Time-Aware Insrumentation of Programs}, - booktitle = {{RTAS'09: 15h IEEE Real-Time and Embedded Technology and Application Symposium} }, - OPTpages = {}, - year = {2009} - } - - -@InProceedings{ZhuDG10, - author = {H. Zhu and M. Dwyer and S. Goddard}, - title = {Predictable Runtime Monitoring}, - booktitle = {ECRTS'09: 21st Euromicro Conference on Real-Time Systems}, - pages = {173--183}, - year = {2009} - } - - - - -%---------- Model Checking, k-induction and IC3 -@INPROCEEDINGS{ClarkeBounded01, - author = {Edmund Clarke and Armin Biere and Richard Raimi and Yunshan Zhu}, - title = {Bounded Model Checking Using Satisfiability Solving}, - booktitle = {Formal Methods in System Design}, - year = {2001}, - publisher = {Kluwer Academic Publishers} -} - -@article{ClarkeBounded03, - author = {Armin Biere and - Alessandro Cimatti and - Edmund M. Clarke and - Ofer Strichman and - Yunshan Zhu}, - title = {Bounded model checking}, - journal = {Advances in Computers}, - year = {2003}, - volume = {58}, - pages = {117--148} -} - - -@Book{ClarkeMC, - author = {E.M. Clarke and O. Grumberg and D. Peled}, - title = {Model Checking}, - publisher = {MIT Press}, - year = {1999} -} - -@PhdThesis{HagenPhD, - author = {G. Hagen}, - title = {Verifying safety properties of Lustre programs: an SMT-based - approach}, - school = {University of Iowa}, - year = {2008} -} - - -@inproceedings{Canovas-Dumas:2000, - author = {Canovas-Dumas, C{\'e}cile and Caspi, Paul}, - title = {A PVS Proof Obligation Generator for Lustre Programs}, - booktitle = {Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning}, - series = {LPAR'00}, - year = {2000}, - isbn = {3-540-41285-9}, - location = {Reunion Island, France}, - pages = {179--188}, - publisher = {Springer-Verlag} -} - - -@inproceedings{Sheeran00, - author = {M. Sheeran and S. Singh and G. St{\aa}lmarck }, - title = {Checking Safety Properties Using Induction and a {SAT}-Solver}, - booktitle = {Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design}, - series = {FMCAD '00}, - year = {2000}, - pages = {108--125}, - publisher = {Springer-Verlag} -} - -@article{EenS03, - author = {Niklas E{\'{e}}n and - Niklas S{\"{o}}rensson}, - title = {Temporal induction by incremental {SAT} solving}, - journal = {Electr. Notes Theor. Comput. Sci.}, - year = {2003}, - volume = {89}, - number = {4}, - pages = {543--560} -} - -@inproceedings{Hagen08, - author = {G. Hagen and C. Tinelli}, - title = {Scaling up the formal verification of Lustre programs with SMT-based techniques}, - year = {2008}, - booktitle = {Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD 08)}, - publisher = {IEEE} -} - - -@inproceedings{BradleyCAV12, - author = {A. R. Bradley}, - title = {IC3 and Beyond: Incremental, Inductive Verification}, - booktitle = {Proceedings of the 24th International Conference on Computer Aided Verification}, - series = {CAV'12}, - year = {2012}, - isbn = {978-3-642-31423-0}, - location = {Berkeley, CA}, - pages = {4--4}, - numpages = {1}, - publisher = {Springer-Verlag} -} - -@inproceedings{Somenzi-FMCAD11, - author = {F. Somenzi and A. R. Bradley}, - title = {IC3: Where Monolithic and Incremental Meet}, - booktitle = {Proceedings of the International Conference on Formal Methods in Computer-Aided Design}, - series = {FMCAD '11}, - year = {2011}, - pages = {3--8}, - publisher = {FMCAD Inc}, - numpages = {6} -} - -@incollection{bradley2012understanding, - title={Understanding ic3}, - author={A. R. Bradley}, - booktitle={Theory and Applications of Satisfiability Testing--SAT 2012}, - pages={1--14}, - year={2012}, - publisher={Springer Berlin Heidelberg} -} - -%Incremental -@INPROCEEDINGS{Bradley06, - author = {A. R. Bradley and Z. Manna}, - title = {Verification constraint problems with strengthening}, - booktitle = {In ICTAC, volume 4281of LNCS}, - pages={ 35--49}, - year = {2006}, - publisher = {Springer-Verlag} -} - - -@inproceedings{Bradley2011, - author = {A. R. Bradley and F. Somenzi and Z. Hassan and Y. Zhang}, - title = {An Incremental Approach to Model Checking Progress Properties}, - booktitle = {Proceedings of the International Conference on Formal Methods in Computer-Aided Design}, - series = {FMCAD '11}, - year = {2011}, - isbn = {978-0-9835678-1-3}, - location = {Austin, Texas}, - pages = {144--153}, - publisher = {FMCAD Inc} -} - - - - -%path compression -@InProceedings{dMRS03, - author = "Leonardo de Moura and Harald Rue{\ss} and Maria - Sorea", - title = "Bounded Model Checking and Induction: From Refutation to Verification", - editor = "Andrei Voronkov", - booktitle = "Computer-Aided Verification, CAV 2003", - year = "2003", - series = "Lecture Notes in Computer Science", - volume = "2725", - publisher = "Springer-Verlag", - pages = "14--26" -} - -%CEGAR -@article{Clarke2003CAR, - author = {E. Clarke and O. Grumberg and S. Jha and Y. Lu and H Veith}, - title = {Counterexample-guided Abstraction Refinement for Symbolic Model Checking}, - journal = {J. ACM}, - issue_date = {September 2003}, - volume = {50}, - number = {5}, - month = sep, - year = {2003}, - issn = {0004-5411}, - pages = {752--794}, - publisher = {ACM} -} - -@inproceedings{bh07structural, - author = {Domagoj Babi\'c and Alan J. Hu}, - title = {{Structural Abstraction of Software Verification Conditions}}, - booktitle = {Proceedings of the 19th International - Conference on Computer Aided Verification}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - location = {Berlin, Germany}, - month = {July}, - year = {2007}, - volume = {4590}, - pages = {371--383} -} - - - -%------------------- -% GADT -%------------------- -@inproceedings{Johann2008, - author = {P. Johann and N. Ghani}, - title = {Foundations for Structured Programming with {GADT}s}, - booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, - series = {POPL '08}, - year = {2008}, - pages = {297--308} -} - -@inproceedings{Xi2003, - author = {H. Xi and C. Chen and G. Chen}, - title = {Guarded Recursive Datatype Constructors}, - booktitle = {Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, - series = {{POPL} '03}, - year = {2003}, - pages = {224--235}, - numpages = {12} -} - -@TechReport{CheneyHinze03, - author = {J. Cheney and R. Hinze}, - title = {First-Class Phantom Types}, - institution = {Cornell University}, - year = {2003}, - number = {{TR}3003-1901} -} - -@misc{Hesselink2005, - title = {The {B}oyer-{M}oore Majority Vote Algorithm}, - author = {Wim H. Hesselink}, - year = {2005} -} - -@techreport{MooreBoyer82, - author = {Moore, Strother J. and Boyer, Robert S.}, - institution = {Institute for Computing Science, University of Texas}, - location = {Austin}, - month = feb, - number = {1981-32}, - pages = {22}, - priority = {2}, - title = {{MJRTY - A Fast Majority Vote Algorithm}}, - year = {1981} -} - -@InProceedings{Dutertre:cav2014, - author = {Dutertre, Bruno}, - title = {Yices 2.2}, - booktitle = {Computer-Aided Verification (CAV'2014)}, - editor = {Biere, Armin and Bloem, Roderick}, - year = 2014, - volume = 8559, - series = {Lecture Notes in Computer Science}, - pages = {737--744}, - month = {July}, - publisher = {Springer}} - -@Misc{kind, - author = {University of Iowa: Kind Research Group}, - title = {Kind 2: {M}ulti-engine {SMT}-based {A}utomatic {M}odel {C}hecker}, - note = {\url{http://kind2-mc.github.io/kind2/}} -} - - - - -@Article{AkbarpourPaulson, - author = {{B}ehzad {A}kbarpour and {L.C. P}aulson}, - title = {{M}eti{T}arski: an Automatic Theorem Prover for Real-Valued Special Functions}, - journal = {Journal of Automated Reasoning}, - year = {2010}, - volume = {44}, - number = {3}, - pages = {175-205} -} - - -%------------------ Recent related MC embedded in PL ----------------- -@inproceedings{Torlak, - author = {{E}mina {T}orlak and {R}astislav {B}odik}, - title = {A Lightweight Symbolic Virtual Machine for Solver-aided Host Languages}, - booktitle = {Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation}, - series = {PLDI '14}, - year = {2014}, - pages = {530--541}, - publisher = {ACM} -} - - - -@inproceedings{Uhler, - author = {{R}ichard {U}hler and {N}irav {D}ave}, - title = {Smten with Satisfiability-based Search}, - booktitle = {Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages \& Applications}, - series = {OOPSLA '14}, - year = {2014}, - pages = {157--176}, - publisher = {ACM} -} - - - -% --------- EDSL ----------- - -@article{Gill:14:DSLs, - author = {Gill, Andy}, - title = {Domain-specific Languages and Code Synthesis Using {H}askell}, - journal = {Commun. ACM}, - volume = {57}, - number = {6}, - month = {June}, - year = {2014}, - issn = {0001-0782}, - pages = {42--49}, - publisher = {ACM} -} - - -@InProceedings{feldspar, - author = {E. Axelsson and K. Claessen and G. Dévai and Z. Horváth and K. Keijzer and B. Lyckegård and A. Persson and M. Sheeran -and J. Svenningsson and A. Vajda}, - title = {{Feldspar:} A Domain Specific Language for Digital Signal Processing algorithms}, - booktitle = {8th ACM/IEEE Int. Conf. on Formal Methods and Models for Codesign}, - year = {2010} -} - -@inproceedings{pike-plpv14, - author = {Lee Pike and - Patrick C. Hickey and - James Bielman and - Trevor Elliott and - Thomas DuBuisson and - John Launchbury}, - title = {Programming languages for high-assurance autonomous vehicles: extended abstract}, - booktitle = {Programming Languages meets Program Verification}, - publisher = {ACM}, - year = {2014}, - pages = {1-2} -} -% note = {Available at \url{http://www.cs.indiana.edu/~lepike/pub_pages/plpv14.html}} diff --git a/WC-End2End/paper.tex b/WC-End2End/paper.tex deleted file mode 100644 index 0118b17..0000000 --- a/WC-End2End/paper.tex +++ /dev/null @@ -1,258 +0,0 @@ -\documentclass[12pt]{article} - -\usepackage{booktabs} -\usepackage[usenames,dvipsnames]{xcolor} -\usepackage[textsize=footnotesize]{todonotes} -\usepackage[utf8]{inputenc} -\usepackage{url} -\usepackage{graphicx} -\usepackage{amssymb} -\usepackage{amsmath} -\usepackage{amsthm} -\usepackage{setspace} -\onehalfspacing -\usepackage{natbib} -\bibliographystyle{plain} -\usepackage{framed} -\usepackage[titles]{tocloft} -\setlength{\cftbeforesecskip}{0.1ex} -\renewcommand{\cftsecfont}{\rm} -\renewcommand{\cftsubsecfont}{\rm} -\renewcommand{\cftdot}{\ensuremath{\dots}} -\renewcommand{\cftsecdotsep}{3} -\renewcommand{\cftsubsecdotsep}{3} -\renewcommand{\cftsecpagefont}{\sl} -\renewcommand{\cftsubsecpagefont}{\sl} -\usepackage{sectsty} -\sectionfont{\large\it\centering} -\subsectionfont{\normalsize\it\centering} -\usepackage{listings} -\usepackage{fancyvrb} -\usepackage[margin=2cm]{geometry} -\usepackage[titletoc]{appendix} -%\usepackage{bcprules} -\usepackage{tikz} -\usepackage{pgf} -\usetikzlibrary{arrows,automata} -\usepackage{tikz-cd} -\usetikzlibrary{positioning} -% boxes around figs -\usepackage{float} -\floatstyle{boxed} -\restylefloat{figure} - - -\DefineVerbatimEnvironment{code}{Verbatim}{fontsize=\footnotesize} - -% Copilot + formatting for listings -\lstdefinelanguage{Copilot} { - language = Haskell, - morekeywords = {arg, Bool, Double, Float, Int8, Int16, Int32, Int64, - Word8, Word16, Word32, Word64, Spec, Stream, String, - Proof, Universal, Existential, - true, false, label, Nothing, Just, arg, constant, drop, - trigger, observer, prop, theorem, interpret, reify, local, - extern, externB, externI8, externI16, externI32, externI64, - externW8, externW16, externW32, externW64, externF, externD, - externFun, externArray, externArrayB, externArrayI8, - externArrayI16, externArrayI32, externArrayI64, externArrayW8, - externArrayW16, externArrayW32, externArrayW64, externArrayF, - externArrayD, not, abs, signum, complement, recip, exp, sqrt, - log, sin, cos, tan, asin, acos, atan, sinh, cosh, tanh, asin, - acosh, atanh, cast, unsafeCast, mod, div, logBase, xor, mux}, - % formatting - commentstyle = \color{ForestGreen}\it, - keywordstyle = \color{blue}\bf, - literate = {+}{{$+$}}1 {/}{{$/$}}1 {*}{{$*$}}1 {=}{{$=$}}1 - {>}{{$>$}}1 {<}{{$<$}}1 {\\}{{${\color{blue}\lambda}$}}1 - {\\\\}{{\char`\\\char`\\}}1 - {\ .}{{$\circ$}}2 {\ .\ }{{$\circ$}}2 - {>>}{{>>}}2 {>>=}{{>>=}}2 - {++}{{${\color{blue}++}$}}2 - {|}{{$\mid$}}1 - {==>}{{${\color{blue}==>}$}}3 -} - -% A custom version of Haskell for listings -\lstdefinelanguage{Haskell} { - morekeywords = {as, case, of, class, data, data, family, data, instance, - default, deriving, do, forall, foreign, hiding, if, then, else, import, - infix, infixl, infixr, let, in, mdo, module, newtype, proc, qualified, - rec, type, where}, - morecomment=[l]{--}, - morecomment=[s]{{\{-}{-\}}}, - morestring=[b]", - literate= {'c}{{$\gamma$}}1 - {'d}{{$\delta$}}1 {'e}{{$\eta$}}1 -} - -%\lstnewenvironment{code} -% {\lstset{}% -% \csname lst@SetFirstLabel\endcsname} -% {\csname lst@SaveFirstLabel\endcsname} -%\lstnewenvironment{Haskell} -%{ -%\lstset{ -% language=Haskell, -% basicstyle=\small\ttfamily, -% flexiblecolumns=false, -% basewidth={0.5em,0.45em} -%} -%} -%{} - - -\definecolor{mygreen}{rgb}{0,0.6,0} -\definecolor{mygray}{rgb}{0.5,0.5,0.5} -\definecolor{mymauve}{rgb}{0.58,0,0.82} - -% Global listings settings -\lstset{ - basewidth={0.5em,0.45em}, % spacing more like verbatim - basicstyle=\footnotesize\ttfamily,% the size/face of the fonts that are used for the code - backgroundcolor=\color{white}, % choose the background color; you must add \usepackage{color} or \usepackage{xcolor} - breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace - breaklines=true, % sets automatic line breaking - captionpos=b, % sets the caption-position to bottom - commentstyle=\color{mygreen}, % comment style - %deletekeywords={ls,xor,conj,reset,gt,input}, % if you want to delete keywords from the given language - escapeinside={\%*}{*)}, % if you want to add LaTeX within your code - extendedchars=true, % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8 - frame=single, % adds a frame around the code - keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible) - keywordstyle=\color{blue}, % keyword style - rulecolor=\color{black}, % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here)) - showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces' - showstringspaces=false, % underline spaces within strings only - showtabs=false, % show tabs within strings adding particular underscores - stringstyle=\color{red}, % string literal style - tabsize=2, % sets default tabsize to 2 spaces -} - - -\newtheoremstyle{example}{\topsep}{\topsep} - {\normalsize\sl} % Body font. - {} % Indent amount (empty = no indent, \parindent = para indent). - {\small\it} % Thm head font. - {:} % Punctuation after thm head. - {\newline} % Space after thm head (\newline = linebreak). - {\thmname{#1} \thmnumber{#2}\thmnote{#3}} % Thm head spec. -\theoremstyle{example} -\newtheorem{example}{Example} - -\newcommand{\hlinepage}{\rule{\textwidth}{0.25pt}} -\newcommand{\HRule}{\rule{\linewidth}{0.25pt}} -\newcommand{\fixme}[1]{\emph{\color{Red}\{!~#1~!\}}} - -\begin{document} - -\thispagestyle{empty} - -\begin{center} - -University of Missouri / ENS Paris / Galois Inc. / NASA LaRC - -\vspace{0.1cm} - -\HRule - -\vspace{0.6cm} - -{\Huge \bfseries -Assured Runtime Verification } -\HRule - -\vspace{0.6cm} -\begin{minipage}{0.3\textwidth} -\large -\begin{center} -Chris Hathhorn \\ -\small{ -hathhorn@gmail.com\\ -} -\end{center} -\end{minipage} -\begin{minipage}{0.3\textwidth} -\large -\begin{center} -Georges-Axel Jaloyan \\ -\small{ -georges-axel.jaloyan@ens.fr\\ -} -\end{center} -\end{minipage} - -\vspace{1cm} - -\begin{minipage}{0.3\textwidth} -\large -\begin{center} -Lee Pike\\ -\small{ -leepike@galois.com\\ -} -\end{center} -\end{minipage} -\vspace{1cm} - - -\begin{minipage}{0.3\textwidth} -\large -\begin{center} -Alwyn E. Goodloe\\ -\small{ -a.goodloe@nasa.gov\\ -} -\end{center} -\end{minipage} -\vspace{1cm} - -{\large -Hampton, Virginia, United States, \today -} - -%\begin{tabular}{cc} -%\hspace{0.5cm}\includegraphics[width=0.18\textwidth]{figures/nia}\hspace{0.5cm} & -%\hspace{0.5cm}\includegraphics[width=0.2\textwidth]{figures/galois}\hspace{0.5cm} & -%\hspace{0.5cm}\includegraphics[width=0.2\textwidth]{figures/nasa}\hspace{0.5cm} \\ -%\textsc{\large NIA} & -%\textsc{\large Galois Inc.} & -%\textsc{\large NASA LaRC} \\ -%\end{tabular} - - -\end{center} - -\vspace{0.25cm} - -\section*{Abstract} -{ -\small We describe an approach to assured runtime verificaition. Our apporach is illustrated using an example from airspace management. -} - -{ -\small -\setcounter{tocdepth}{2} -\tableofcontents -} - -\newpage -\addcontentsline{toc}{section}{Acknowledgement} -\section*{Acknowledgement} -TBD -{ -\input{intro} -\input{copilot} -\input{wellclear} -\input{specverify} -\input{verifiedmonitors} -\input{CompCert} -\input{flightTest} -\input{conclusion} -\bibliography{paper} -} - -%\begin{appendices} -%\end{appendices} -\end{document} - diff --git a/WC-End2End/pvs/ECEF.pvs b/WC-End2End/pvs/ECEF.pvs deleted file mode 100644 index 4c2908c..0000000 --- a/WC-End2End/pvs/ECEF.pvs +++ /dev/null @@ -1,26 +0,0 @@ -ECEF: THEORY -%---------------------------------------------------------------------------- -% -% Earth-Centered, Earth-Fixed Cartesian coordinate system -% -%---------------------------------------------------------------------------- -BEGIN - - IMPORTING trig@trig_basic, - vectors_3D - - r : VAR posreal % Radius of the Earth - lat,lon : VAR real - - spherical2xyz(r,lat,lon): Nz_vect3 = % Convert LatLon to ECEF - LET theta = pi/2 - lat, - phi = pi-lon, - x = r*sin(theta)*cos(phi), - y = r*sin(theta)*sin(phi), - z = r*cos(theta) - IN (x,y,z) - - spherical2xyz_norm: LEMMA - LET vv = spherical2xyz(r,lat,lon) IN norm(vv) = r - -END ECEF diff --git a/WC-End2End/pvs/vect3_basis.pvs b/WC-End2End/pvs/vect3_basis.pvs deleted file mode 100644 index 0e6df78..0000000 --- a/WC-End2End/pvs/vect3_basis.pvs +++ /dev/null @@ -1,91 +0,0 @@ -vect3_basis: THEORY -%---------------------------------------------------------------------------- -% Given one vector of norm 1, this gives an orthonormal basis containing that vector -% -%---------------------------------------------------------------------------- -BEGIN - - IMPORTING perpendicular_3D, cross_3D - - t,tp: VAR real - P0,Q,v,w,u,c,d,x,y,del: VAR Vect3 - nzv,nzw,nzu: VAR Nz_vect3 - R : VAR posreal % Radius of the sphere to be rotated and planed - - vect3_orthog_tox(v): Vect3 = v - - vect3_orthog_toy(v): Vect3 = - IF v`x/=0 OR v`y /=0 THEN (v`y,-v`x,0) - ELSE (1,0,0) ENDIF - - vect3_orthog_toy_def: LEMMA v/=zero IMPLIES orthogonal?(v,vect3_orthog_toy(v)) - - vect3_orthog_toz(v): Vect3 = cross(v,vect3_orthog_toy(v)) - - vect3_orthog_toz_def: LEMMA orthogonal?(v,vect3_orthog_toz(v)) - AND - orthogonal?(vect3_orthog_toy(v),vect3_orthog_toz(v)) - - - %%%%%%% The normalized basis %%%%%%% - - vect3_orthonorm_tox(nzv): Normalized = ^(nzv) - - vect3_orthonorm_toy(nzv): Normalized = ^(vect3_orthog_toy(nzv)) - - vect3_orthonorm_toz(nzv): Normalized = ^(vect3_orthog_toz(nzv)) - - vect3_orthonorm_basis: LEMMA - LET v = vect3_orthonorm_tox(nzv), - u = vect3_orthonorm_toy(nzv), - w = vect3_orthonorm_toz(nzv) - IN - orthogonal?(v,u) AND orthogonal?(u,w) AND orthogonal?(w,v) - - %%%%%%% Rotation to Equator %%%%%%% - - %%%%%%% A distance preserving map... %%%%%%% - - Equator_map(nzv)(w): Vect3 = - LET xmult: Vect3 = vect3_orthonorm_tox(nzv), - ymult: Vect3 = vect3_orthonorm_toy(nzv), - zmult: Vect3 = vect3_orthonorm_toz(nzv) - IN - (xmult*w,ymult*w,zmult*w) - - Equator_map_def: LEMMA normalized?(nzv) IMPLIES - Equator_map(nzv)(nzv) = (1,0,0) - - transpose_Equator_map(nzv): [Vect3,Vect3,Vect3] = - LET xvect: Vect3 = vect3_orthonorm_tox(nzv), - yvect: Vect3 = vect3_orthonorm_toy(nzv), - zvect: Vect3 = vect3_orthonorm_toz(nzv), - xmultinv: Vect3 = (xvect`x,yvect`x,zvect`x), - ymultinv: Vect3 = (xvect`y,yvect`y,zvect`y), - zmultinv: Vect3 = (xvect`z,yvect`z,zvect`z) - IN (xmultinv,ymultinv,zmultinv) - - Equator_map_inv(nzv)(w): Vect3 = - LET xvect: Vect3 = vect3_orthonorm_tox(nzv), - yvect: Vect3 = vect3_orthonorm_toy(nzv), - zvect: Vect3 = vect3_orthonorm_toz(nzv), - xmultinv: Vect3 = (xvect`x,yvect`x,zvect`x), - ymultinv: Vect3 = (xvect`y,yvect`y,zvect`y), - zmultinv: Vect3 = (xvect`z,yvect`z,zvect`z) - IN - (xmultinv*w,ymultinv*w,zmultinv*w) - - Equator_map_inv_def: LEMMA - Equator_map(nzv)(Equator_map_inv(nzv)(w)) = w - - - %%%%%%% Translating to 2D Plane %%%%%%% - - sphere_to_2D_plane(nzv)(w): Vect2 = - LET xmult: Vect3 = vect3_orthonorm_tox(nzv), - ymult: Vect3 = vect3_orthonorm_toy(nzv), - zmult: Vect3 = vect3_orthonorm_toz(nzv) - IN - (ymult*w,zmult*w) - -END vect3_basis diff --git a/WC-End2End/pvs/vectors_3D.pvs b/WC-End2End/pvs/vectors_3D.pvs deleted file mode 100644 index cf346c8..0000000 --- a/WC-End2End/pvs/vectors_3D.pvs +++ /dev/null @@ -1,442 +0,0 @@ -vectors_3D: THEORY -%---------------------------------------------------------------------------- -% -% The Vect3 type is a record [# x, y, z: real #] -% but the vect3 conversion allows one to write (x,y,z) -% -%---------------------------------------------------------------------------- -BEGIN - - IMPORTING reals@sqrt, vectors_3D_def - - Vector : TYPE = Vect3 - u,v,w : VAR Vector - a,b,c : VAR real - nza : VAR nzreal - -% ----------- Special vectors --------------------------------------------- - - zero: Vector = (0,0,0) - const_vec(a): Vector = (a,a,a) ; - -% ----------- Vector Operations ------------------------------------------- - - -(v) : Vector = ( -v`x, -v`y, -v`z ) ; - - +(u,v): Vector = ( u`x + v`x, u`y + v`y, u`z + v`z ) ; - - -(u,v): Vector = ( u`x - v`x, u`y - v`y, u`z - v`z ) ; - - *(u,v): real = u`x * v`x + u`y * v`y + u`z * v`z ; % dot product - - *(a,v): Vector = ( a * v`x, a * v`y, a * v`z ) ; - -% ----------- Vector Functions ------------------------------------------- - - sqv(v): nnreal = v*v - - sos(v): nnreal = sq(v`x)+sq(v`y)+sq(v`z) - - sqv_rew : LEMMA v*v = sqv(v) - - sqv_sos : LEMMA sqv(v) = sos(v) - - norm(v): nnreal = sqrt(sqv(v)) - - zero_vector?(v): MACRO bool = - v = zero - - nz_vector?(v): MACRO bool = - v /= zero - - zero_vect3? : MACRO PRED[Vector] = zero_vector? - nz_vect3? : MACRO PRED[Vector] = nz_vector? - - normalized?(v): MACRO bool = - norm(v) = 1 - - Nz_vector : TYPE = (nz_vector?) - Nz_vect3 : TYPE = Nz_vector - Normalized : TYPE = (normalized?) - - iv: Vector = (1,0,0) - jv: Vector = (0,1,0) - kv: Vector = (0,0,1) - - nzu,nzv : VAR Nz_vector - -% ----------- Vector Component Lemmas - - basis : LEMMA a*iv + b*jv +c*kv = (a,b,c) - - vx_distr_add : LEMMA (v + w)`x = v`x + w`x - vy_distr_add : LEMMA (v + w)`y = v`y + w`y - vz_distr_add : LEMMA (v + w)`z = v`z + w`z - - vx_distr_sub : LEMMA (v - w)`x = v`x - w`x - vy_distr_sub : LEMMA (v - w)`y = v`y - w`y - vz_distr_sub : LEMMA (v - w)`z = v`z - w`z - - vx_scal : LEMMA (a*v)`x = a*v`x - vy_scal : LEMMA (a*v)`y = a*v`y - vz_scal : LEMMA (a*v)`z = a*v`z - - vx_neg : LEMMA (-v)`x = -v`x - vy_neg : LEMMA (-v)`y = -v`y - vz_neg : LEMMA (-v)`z = -v`z - - comp_eq_x : LEMMA u = w IMPLIES u`x = w`x - comp_eq_y : LEMMA u = w IMPLIES u`y = w`y - comp_eq_z : LEMMA u = w IMPLIES u`z = w`z - - comps_eq : LEMMA u = w IFF u`x = w`x AND u`y = w`y AND u`z = w`z - - comp_zero_x : LEMMA zero`x = 0 - comp_zero_y : LEMMA zero`y = 0 - comp_zero_z : LEMMA zero`z = 0 - - norm_xyz_eq_0 : LEMMA norm(v) = 0 IFF v`x =0 AND v`y=0 AND v`z=0 - - norm_sqv_eq_0 : LEMMA norm(v) = 0 IFF sqv(v) = 0 - - norm_eq_0 : LEMMA norm(v) = 0 IFF v = zero - - norm_zero : LEMMA norm(zero) = 0 - - sqv_zero : LEMMA sqv(zero) = 0 - - sqv_eq_0 : LEMMA sqv(v) = 0 IFF v = zero - - v_neq_zero : LEMMA v /= zero IFF sqv(v) > 0 - - sq_dot_eq_0 : LEMMA v*v = 0 IFF v = zero - - nzv_xyz_neq_0 : LEMMA nz_vector?(v) IFF v`x /= 0 OR v`y /= 0 OR v`z /= 0 - -% ----------- JUDGEMENTS ------------------------------------- - - nz_norm_gt_0 : JUDGEMENT - norm(nzu) HAS_TYPE posreal - - nz_sqv_gt_0 : JUDGEMENT - sqv(nzu) HAS_TYPE posreal - - nz_nvz_left : JUDGEMENT - mk_vect3(nza,b,c) HAS_TYPE Nz_vector - - nz_nvz_middle : JUDGEMENT - mk_vect3(b,nza,c) HAS_TYPE Nz_vector - - nz_nvz_right : JUDGEMENT - mk_vect3(b,c,nza) HAS_TYPE Nz_vector - - normalized_nz : JUDGEMENT - Normalized SUBTYPE_OF Nz_vector - - neg_nzv : JUDGEMENT - -(nzu) HAS_TYPE Nz_vector - - nz_nzv : JUDGEMENT - *(nza,nzv) HAS_TYPE Nz_vector - -% ----------- Vector Operation Lemmas ------------------------------------- - - neg_zero : LEMMA -zero = zero - - add_zero_left : LEMMA zero + v = v - - add_zero_right : LEMMA v + zero = v - - add_comm : LEMMA u+v = v+u - - add_assoc : LEMMA u+(v+w) = (u+v)+w - - add_move_left : LEMMA u + w = v IFF w = v - u - - add_move_right : LEMMA u + w = v IFF u = v - w - - add_move_both : LEMMA v = u + w IFF u = v - w - - add_neg_sub : LEMMA v + -u = v - u - - add_cancel : LEMMA v + w - v = w - - add_cancel_neg : LEMMA -v + w + v = w - - add_cancel2 : LEMMA w - v + v = w - - add_cancel_neg2 : LEMMA w + v - v = w - - add_cancel_left : LEMMA u + v = u + w IMPLIES v = w - - add_cancel_right : LEMMA u + v = w + v IMPLIES u = w - - add_eq_zero : LEMMA u + v = zero IFF u = -v - - neg_shift : LEMMA u = -v IFF -u = v - - - sub_cancel_left : LEMMA u - v = u - w IMPLIES v = w - - sub_cancel_right : LEMMA u - v = w - v IMPLIES u = w - - sub_zero_left : LEMMA zero - v = -v - - sub_zero_right : LEMMA v - zero = v - - sub_eq_args : LEMMA v - v = zero - - sub_eq_zero : LEMMA u - v = zero IFF u = v - - sub_cancel : LEMMA v - w - v = -w - - sub_cancel_neg : LEMMA -v - w + v = -w - - - neg_add_left : LEMMA -v + v = zero - - neg_add_right : LEMMA v + -v = zero - - neg_distr_sub : LEMMA -(v - u) = u - v - - neg_neg : LEMMA --v = v - - neg_distr_add : LEMMA -(u + v) = -u - v - - dot_neg_left : LEMMA (-u)*w = -(u*w) - - dot_neg_right : LEMMA u*(-w) = -(u*w) - - neg_dot_neg : LEMMA (-u)*(-v) = u*v - - dot_zero_left : LEMMA zero * v = 0 - - dot_zero_right : LEMMA v * zero = 0 - - dot_comm : LEMMA u*v = v*u - - dot_assoc : LEMMA a*(v*w) = (a*v)*w - - dot_eq_args_ge : LEMMA u*u >= 0 - - add_comm_assoc_left : LEMMA (u+v)+w = (u+w)+v - - add_comm_assoc_right: LEMMA u+(v+w) = v+(u+w) - - dot_add_right : LEMMA u*(v+w) = u*v + u*w - - dot_add_left : LEMMA (v+w)*u = v*u + w*u - - dot_sub_right : LEMMA u*(v-w) = u*v - u*w - - dot_sub_left : LEMMA (v-w)*u = v*u - w*u - - dot_divby : LEMMA nza*u = nza*v IMPLIES u = v - - dot_scal_left : LEMMA (a*u)*v = a*(u*v) - - dot_scal_right : LEMMA u*(a*v) = a*(u*v) - - dot_scal_comm_assoc : LEMMA (a*u)*v = (a*v)*u - - scal_comm_assoc : LEMMA a*(b*u) = b*(a*u) - - dot_scal_canon : LEMMA (a*u)*(b*v) = (a*b)*(u*v) - - scal_add_left : LEMMA (a+b)*u = a*u + b*u - - scal_sub_left : LEMMA (a-b)*u = a*u - b*u - - scal_add_right : LEMMA a*(u+v) = a*u + a*v - - scal_sub_right : LEMMA a*(u-v) = a*u - a*v - - scal_assoc : LEMMA a*(b*u) = (a*b)*u - - scal_neg : LEMMA a*(-v) = (-a)*v - - scal_cross : LEMMA (1/nza) * v = w IFF v = nza*w - - scal_zero : LEMMA a * zero = zero - - scal_0 : LEMMA 0 * v = zero - - scal_1 : LEMMA 1 * v = v - - scal_neg_1 : LEMMA -1 * v = -v - - scal_cancel : LEMMA a*nzv = b*nzv IMPLIES a = b - - scal_div_mult_left : LEMMA (a/nza)*u = v IFF a*u = nza*v %%% - - scal_div_mult_right : LEMMA u = (a/nza)*v IFF nza*u = a*v %%% - - scal_eq_zero : LEMMA c*v = zero IMPLIES c = 0 OR v = zero - - dot_ge_dist : LEMMA w*u >= w*v IMPLIES w*(u-v) >= 0 - - dot_gt_dist : LEMMA w*u > w*v IMPLIES w*(u-v) > 0 - - idem_right : LEMMA a * v = v IFF (a = 1 OR v = zero) - - sqv_neg : LEMMA sqv(-v) = sqv(v) - - sqv_add : LEMMA sqv(u+v) = sqv(u) + sqv(v) + 2*u*v - - sqv_scal : LEMMA sqv(a*v) = sq(a)*sqv(v) - - sqv_sub : LEMMA sqv(u-v) = sqv(u) + sqv(v) - 2*u*v - - sqv_sub_scal : LEMMA sqv(u-a*v) = sqv(u) - 2*a*u*v + sq(a)*sqv(v) - - sqv_sym : LEMMA sqv(u-v) = sqv(v-u) - - sqrt_sqv_sq : LEMMA sqrt(sqv(v)) * sqrt(sqv(v)) = sqv(v) - - norm_sym : LEMMA norm(u-v) = norm(v-u) - - norm_neg : LEMMA norm(-u) = norm(u) - - dot_sq_norm : LEMMA u*u = sq(norm(u)) - - sq_norm : LEMMA sq(norm(u)) = sqv(u) - - sqrt_sqv_norm : LEMMA sqrt(sqv(v)) = norm(v) - - norms_eq_sqv : LEMMA norm(u) = norm(v) IFF sqv(u) = sqv(v) - - norms_eq_sos : LEMMA norm(u) = norm(v) IFF sos(u) = sos(v) - - norm_le_sqv : LEMMA norm(u) <= norm(v) IFF sqv(u) <= sqv(v) - - norm_lt_sqv : LEMMA norm(u) < norm(v) IFF sqv(u) < sqv(v) - - norm_scal : LEMMA norm(a*v) = abs(a)*norm(v) ; - - ^(nzv) : Normalized = (1/norm(nzv))*nzv - - normalize(nzv) : MACRO Normalized = ^(nzv) - - norm_normalize : LEMMA - norm(^(nzv)) = 1 - - dot_normalize : LEMMA - ^(nzu) * ^(nzv) = nzu*nzv/(norm(nzu)*norm(nzv)) - - normalize_normalize: LEMMA ^(^(nzv)) = ^(nzv) - - normalized_id : LEMMA norm(nzv)*^(nzv) = nzv - - normalize_scal : LEMMA ^(nza*nzv) = sign(nza)*^(nzv) - - cauchy_schwarz : LEMMA sq(u*v) <= sqv(u)*sqv(v) - - dot_norm : LEMMA -norm(u)*norm(v) <= u*v AND u*v <= norm(u)*norm(v) - - schwarz : LEMMA abs(u*v) <= norm(u)*norm(v) - - schwarz_cor : LEMMA sqrt(sqv(u+v)) <= sqrt(sqv(u)) + sqrt(sqv(v)) - - norm_triangle : LEMMA norm(u-w) <= norm(u-v) + norm(v-w) - - norm_add_le : LEMMA norm(u+v) <= norm(u) + norm(v) - - norm_sub_le : LEMMA norm(u-v) <= norm(u) + norm(v) - - norm_sub_ge : LEMMA norm(u-v) >= norm(u) - norm(v) - - norm_ge_comps : LEMMA norm(u) >= abs(u`x) AND - norm(u) >= abs(u`y) AND - norm(u) >= abs(u`z) - - v0,v1,v2 : VAR Vect3 - sq_norm_dist : LEMMA LET a = v1-v0, b = v1-v2, c = v2-v0 IN - sq(norm(c)) = sq(norm(a)) + sq(norm(b)) - 2*a*b - -% ---------- Predicates over vectors --------- - - parallel?(u,v): bool = - EXISTS (nzk:nzreal): u = nzk*v - - dir_parallel?(u,v): bool = - EXISTS (pk:posreal): u = pk*v - - parallel_refl : LEMMA - parallel?(u,u) - - parallel_symm : LEMMA - parallel?(u,v) IFF parallel?(v,u) - - parallel_trans : LEMMA - parallel?(u,v) AND parallel?(v,w) IMPLIES - parallel?(u,w) - - parallel_zero : LEMMA - parallel?(u,zero) IFF u = zero - - dir_parallel : LEMMA - dir_parallel?(u,v) IMPLIES parallel?(u,v) - - orthogonal?(u,v): bool = u * v = 0 - - pythagorean : LEMMA - orthogonal?(u,v) IMPLIES - sqv(u+v) = sqv(u) + sqv(v) - - norm_add_ge_left : LEMMA - orthogonal?(u,v) IMPLIES - norm(u+v) >= norm(u) - - norm_add_ge_right : LEMMA - orthogonal?(u,v) IMPLIES - norm(u+v) >= norm(v) - -% ---------- Auto Rewrites ----------------------- - - AUTO_REWRITE+ neg_zero - AUTO_REWRITE+ add_zero_left - AUTO_REWRITE+ add_zero_right - AUTO_REWRITE+ sub_zero_left - AUTO_REWRITE+ sub_zero_right - AUTO_REWRITE+ sub_eq_args - AUTO_REWRITE+ neg_add_left - AUTO_REWRITE+ neg_add_right - AUTO_REWRITE+ dot_zero_left - AUTO_REWRITE+ dot_zero_right - AUTO_REWRITE+ scal_zero - AUTO_REWRITE+ scal_0 - AUTO_REWRITE+ scal_1 - AUTO_REWRITE+ scal_neg_1 - AUTO_REWRITE+ sqv_zero - AUTO_REWRITE+ norm_zero - AUTO_REWRITE+ add_neg_sub - AUTO_REWRITE+ neg_neg - AUTO_REWRITE+ dot_scal_left - AUTO_REWRITE+ dot_scal_right - AUTO_REWRITE+ dot_scal_canon - AUTO_REWRITE+ scal_assoc - AUTO_REWRITE+ sqv_neg - AUTO_REWRITE+ sqrt_sqv_sq - AUTO_REWRITE+ norm_neg - AUTO_REWRITE+ norm_normalize - AUTO_REWRITE+ comp_zero_x - AUTO_REWRITE+ comp_zero_y - AUTO_REWRITE+ comp_zero_z - AUTO_REWRITE+ add_cancel - AUTO_REWRITE+ sub_cancel - AUTO_REWRITE+ add_cancel_neg - AUTO_REWRITE+ sub_cancel_neg - AUTO_REWRITE+ add_cancel2 - AUTO_REWRITE+ add_cancel_neg2 - -% ---- Turn off dangerous and unhelpful rewrites for auto-rewrite-theory -- - - AUTO_REWRITE- add_comm % LEMMA u+v = v+u - AUTO_REWRITE- dot_comm % LEMMA u*v = v*u - AUTO_REWRITE- dot_assoc % LEMMA a*(v*w) = (a*v)*w - AUTO_REWRITE- sqv_sym % LEMMA sqv(u-v) = sqv(v-u) - AUTO_REWRITE- norm_sym % LEMMA norm(u-v) = norm(v-u) - AUTO_REWRITE- dot_sq_norm % LEMMA u*u = sq(norm(u)) - -END vectors_3D - diff --git a/WC-End2End/specverify.tex b/WC-End2End/specverify.tex deleted file mode 100644 index c40b2ad..0000000 --- a/WC-End2End/specverify.tex +++ /dev/null @@ -1,10 +0,0 @@ -\section{Assuring Specifications}~\label{sec:specverify} - -How we assure our specfications using SMT based tools\citep{assuring-guardians}. - - -\subsection{Assured Well Clear}~\label{sec:verifiywc} - -How we applied Z3 to assure WC spec. - - diff --git a/WC-End2End/verifiedmonitors.tex b/WC-End2End/verifiedmonitors.tex deleted file mode 100644 index e1a3ce8..0000000 --- a/WC-End2End/verifiedmonitors.tex +++ /dev/null @@ -1,9 +0,0 @@ -\section{Verified Monitors}~\label{sec:vermon} - -How we leverage the Frama-C deductive verification plug-in wp to verify that the C monitors do indeed implement the high-level monitors. - -Discuss tracability and the use of Frama-C value analysis tool as well. - -\subsection{Well Clear Monitor Example}~\label{sec:verwcmon} - -Examples from the well clear monitors. diff --git a/WC-End2End/wellclear.tex b/WC-End2End/wellclear.tex deleted file mode 100644 index 9d5296d..0000000 --- a/WC-End2End/wellclear.tex +++ /dev/null @@ -1,45 +0,0 @@ -\section{Well Clear}~\label{sec:wellclear} - -Overview of well clear. Probably summarize Cesar's papers on the subject. -Some basic formulas : \newline -$WCV_{t_{\mathrm{var}}} (\mathbf s,s_z,\mathbf v,v_z) \equiv \mathrm{Horizontal\_WCV_\mathit{t_{\mathrm{var}}}}(\mathbf{s},\mathbf v) ~\mathrm{and}~ \mathrm{Vertical\_WCV}(s_z,v_z)$ \newline -$\mathrm{Horizontal\_WCV_\mathit{t_{\mathrm{var}}}}(\mathbf{s},\mathbf v) \equiv \Vert \mathbf s \Vert \leq \mathrm{DTHR} ~ \mathrm{or} ~ -(d_{\mathrm{cpa}}(\mathbf s, \mathbf v) \leq \mathrm{DTHR} ~ \mathrm{and} ~ 0 \leq t_{\mathrm{var}}(\mathbf s, \mathbf v) \leq \mathrm{TTHR})$\newline -$\mathrm{Vertical\_WCV}(s_z,v_z) \equiv \vert s_z \vert \leq \mathrm{ZTHR} ~\mathrm{or}~ 0 \leq t_{\mathrm{coa}}(s_z,v_z) \leq \mathrm{TCOA}$\newline -$d_{\mathrm{cpa}} (\mathbf s, \mathbf v) = \Vert \mathbf s + t_{\mathrm{cpa}}(\mathbf s, \mathbf v) \mathbf v \Vert$ \newline -$t_{\mathrm{coa}}(s_z,v_z) \equiv \left\{ -\begin{array}{ll} -- \frac{s_z}{v_z} & \mathrm{if} ~ {s_z}{v_z} < 0\\ -- 1 & \mathrm{otherwise} -\end{array} -\right. $ \newline -\newline - -With : \newline -$\tau(\mathbf{s},\mathbf v) \equiv \left\{ -\begin{array}{ll} -- \frac{\mathbf{s}^2}{\mathbf{s} \cdot \mathbf{v}} & \mathrm{if} ~ \mathbf{s} \cdot \mathbf{v} < 0\\ -- 1 & \mathrm{otherwise} -\end{array} -\right. $\newline -$t_{\mathrm{cpa}}(\mathbf{s},\mathbf v) \equiv \left\{ -\begin{array}{ll} -- \frac{\mathbf{s} \cdot \mathbf{v}}{\mathbf{v}^2} & \mathrm{if} ~ \mathbf{v} \neq 0\\ -0 & \mathrm{otherwise} -\end{array} -\right. $\newline -$\tau_{\mathrm{mod}}(\mathbf{s},\mathbf v) \equiv \left\{ -\begin{array}{ll} -\frac{\mathrm{DTHR}^2-\mathbf{s}^2}{\mathbf{s} \cdot \mathbf{v}} & \mathrm{if} ~ \mathbf{s} \cdot \mathbf{v} < 0\\ --1 & \mathrm{otherwise} -\end{array} -\right. $ \newline -$t_{\mathrm{ep}}(\mathbf{s},\mathbf v) \equiv \left\{ -\begin{array}{ll} -\Theta (\mathbf{s},\mathbf{v}, \mathrm{DTHR}, -1) & \mathrm{if} ~ \mathbf{s} \cdot \mathbf{v} < 0 ~\mathrm{and}~ \Delta(\mathbf{s},\mathbf v, \mathrm{DTHR}) \ge 0\\ --1 & \mathrm{otherwise} -\end{array} -\right. $ \newline -$\Theta (\mathbf{s},\mathbf{v}, D, \epsilon) \equiv \frac{-\mathbf{s}\cdot\mathbf{v} + \epsilon \sqrt{\Delta(\mathbf{s},\mathbf{v},D)}}{\mathbf{v}^2}$\newline -$\Delta(\mathbf{s},\mathbf{v},D) \equiv D^2\mathbf{v}^2 - (\mathbf{s}\cdot\mathbf{v}^{\perp})^2 \\ -\Leftrightarrow \Delta(\mathbf{s},\mathbf{v},D) \equiv D^2\mathbf{v}^2 - Det(\mathbf{s},\mathbf{v})^2$