@inproceedings{DBLP:conf/cade/BriegerMP23,
        author    = {Brieger, Marvin and Mitsch, Stefan and Platzer, André},
        title     = {Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs},
        booktitle = {CADE},
        longbooktitle = {},
        year      = {2023},
        pages     = {},
        doi       = {},
        editor    = {},
        publisher = {Springer},
        series    = {LNCS},
        volume    = {},
      }
    

      @inproceedings{DBLP:conf/tap/StraussM23,
        author    = {Strauss, Megan and Mitsch, Stefan},
        title     = {Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars},
        booktitle = {TAP},
        longbooktitle = {TAP 2023 - 17th International Conference on Tests and Proofs, Proceedings},
        year      = {2023},
        pages     = {},
        doi       = {},
        editor    = {},
        publisher = {Springer},
        series    = {LNCS},
        volume    = {},
      }
    

      @inproceedings{DBLP:conf/nfm/QianM23,
        author    = {Qian, Marian and Mitsch, Stefan},
        title     = {Reward Shaping from Hybrid Systems Models in Reinforcement Learning},
        booktitle = {NFM},
        longbooktitle = {NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16--18, 2023, Proceedings},
        year      = {2023},
        pages     = {},
        doi       = {},
        editor    = {Kristin Yvonne Rozier and Swarat Chaudhuri},
        publisher = {Springer},
        series    = {LNCS},
        volume    = {13903},
      }
    

      @inproceedings{DBLP:conf/ersa/Mitsch22,
        author    = {Mitsch, Stefan},
        title     = {Formal Artifacts as Explanations for System 
                     Correctness in Cyber-Physical Systems},
        booktitle = {ERSA},
        longbooktitle = {Explainability of Real-Time Systems and their Analysis},
        year      = {2022},
        pages     = {},
        doi       = {},
        editor    = {},
        publisher = {IEEE},
        series    = {},
        volume    = {},
      }
    

        @inproceedings{DBLP:conf/cade/GallicchioTMP22,
          author    = {Gallicchio, James and
                       Tan, Yong Kiam and
                       Mitsch, Stefan and
                       Platzer, Andr{\'e}},
          title     = {Implicit Definitions with Differential Equations for {KeYmaera} {X}
                       - (System Description)},
          booktitle = {IJCAR},
          longbooktitle = {Automated Reasoning, International
                       Joint Conference, IJCAR 2022, Proceedings},
          year      = {2022},
          pages     = {723-733},
          doi       = {10.1007/978-3-031-10769-6_42},
          editor    = {Jasmin Blanchette and
                       Laura Kov{\'{a}}cs and
                       Dirk Pattinson},
          publisher = {Springer},
          series    = {LNCS},
          volume    = {13385},
        }
      

        @article{DBLP:journals/tcad/KabraMP,
          author    = {Kabra, Aditi and
                       Mitsch, Stefan and
                       Platzer, Andr{\'{e}}},
          title     = {Verified Train Controllers for the
                       Federal Railroad Administration Train Kinematics Model:
                       Balancing Competing Brake and Track Forces}, 
          journal   = {{IEEE} Trans. Comput. Aided Des. Integr. Circuits Syst.},
          longjournal = {{IEEE} Transactions on Computer-Aided Design of
                       Integrated Circuits and Systems}, 
          volume    = {},
          number    = {},
          pages     = {},
          year      = {2022},
          doi       = {10.1109/TCAD.2022.3197690},
          issn      = {0278-0070},
        }
      

        @article{DBLP:journals/tecs/CleavelandMP,
          author    = {Rachel Cleaveland and
                      Stefan Mitsch and
                      Andr{\'e} Platzer},
          title     = {Formally Verified Next-Generation Airborne Collision Avoidance Games in {ACAS X}},
          journal   = {{ACM} Trans. Embed. Comput. Syst.},
          volume    = {},
          number    = {},
          pages     = {},
          year      = {},
          doi       = {10.1145/3544970},
          issn      = {1539-9087},
        }
      

        @article{DBLP:journals/lites/KamburjanMH22,
          author    = {Eduard Kamburjan and
                       Stefan Mitsch and
                       Reiner H{\"a}hnle},
          title     = {A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems},
          journal   = {Leibniz Transactions on Embedded Systems}
          year      = {2022},
          volume    = {},
          number    = {},
          pages     = {},
          doi       = {}
        }
      

        @inproceedings{DBLP:conf/hybrid/TanMP22,
          author    = {Yong Kiam Tan and
                       Stefan Mitsch and
                       Andr{\'e} Platzer},
          title     = {Verifying Switched System Stability With Logic},
          year      = {2022},
          pages     = {},
          doi       = {},
          publisher = {ACM},
          editor    = {Ezio Bartocci and
                       Sylvie Putot},
          booktitle = {Hybrid Systems: Computation and Control
                       (part of CPS Week 2022), HSCC'22}
        }
      

        @inproceedings{DBLP:conf/vmcai/BayaniM22,
          author    = {David Bayani and
                       Stefan Mitsch},
          title     = {Fanoos: Multi-resolution, Multi-strength, Interactive Explanations
                       for Learned Systems},
          booktitle = {Verification, Model Checking, and Abstract Interpretation - 23rd International
                       Conference, {VMCAI} 2022, Philadelphia, PA, USA, January 16-18, 2022,
                       Proceedings},
          pages     = {43--68},
          year      = {2022},
          doi       = {10.1007/978-3-030-94583-1\_3}
        }
      

        @inproceedings{DBLP:conf/arch/MitschJZWZ21,
          author    = {Stefan Mitsch and
                       Xiangyu Jin and
                       Bohua Zhan and
                       Shuling Wang and
                       Naijun Zhan},
          title     = {{ARCH-COMP21} Category Report: Hybrid Systems Theorem Proving},
          booktitle = {8th International Workshop on Applied Verification of Continuous and
                       Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021},
          pages     = {120--132},
          year      = {2021},
          doi       = {10.29007/35cf}
        }
      

        @inproceedings{DBLP:conf/fm/KopylovMNW21,
          author    = {Alexei Kopylov and
                       Stefan Mitsch and
                       Aleksey Nogin and
                       Michael Warren},
          title     = {Formally Verified Safety Net for Waypoint Navigation Neural Network
                       Controllers},
          booktitle = {Formal Methods - 24th International Symposium, {FM} 2021, Virtual
                       Event, November 20-26, 2021, Proceedings},
          pages     = {122--141},
          year      = {2021},
          doi       = {10.1007/978-3-030-90870-6\_7}
        }
      

        @inproceedings{DBLP:conf/fm/ScharagerCMP21,
          author    = {Matias Scharager and
                       Katherine Cordwell and
                       Stefan Mitsch and
                       Andr{\'{e}} Platzer},
          title     = {Verified Quadratic Virtual Substitution for Real Arithmetic},
          booktitle = {Formal Methods - 24th International Symposium, {FM} 2021, Virtual
                       Event, November 20-26, 2021, Proceedings},
          pages     = {200--217},
          year      = {2021},
          doi       = {10.1007/978-3-030-90870-6\_11}
        }
      

        @article{LinMPD21,
          author={Lin, Qin and Mitsch, Stefan and Platzer, André and Dolan, John M.},
          journal={IEEE Control Systems Letters}, 
          title={Safe and Resilient Practical Waypoint-Following for Autonomous Vehicles}, 
          year={2022},
          volume={6},
          number={},
          pages={1574-1579},
          doi={10.1109/LCSYS.2021.3125717}
        }
      

        @inproceedings{DBLP:conf/fide/Mitsch21,
          author = {Stefan Mitsch},
          title = {Implicit and Explicit Proof Management in KeYmaera X},
          booktitle = {6th Workshop on Formal Integrated Development Environment (F-IDE'21)},
          year = {2021},
          note = {To appear}
        }
    

        @inproceedings{DBLP:conf/iiwas/RetschitzeggerSMM20
          author = {Werner Retschitzegger and
                    Wieland Schwinger and
                    Andreas Müller and
                    Stefan Mitsch},
          title = {Towards {CPS} Verification Engineering},
          booktitle = {22nd International Conference on Information Integration and Web-based Applications {\&} Services, Proceedings},
          year = {2020}
        }
    

        @INPROCEEDINGS{DBLP:conf/ijcaixai/BayaniM20,
          author = {David Bayani and
                    Stefan Mitsch},
          title = {Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned Systems},
          booktitle = {IJCAI-PRICAI 2020 Workshop on Explainable Artificial Intelligence (XAI), Proceedings},
          year = {2020},
          url = {https://drive.google.com/file/d/1_RN_8DvF-XV1b_m1_AyrkQ-Tst0dVSJd/view?usp=sharing}
        }
    

        @ARTICLE{DBLP:journals/fmsd/SogokonMTCP,
          author    = {Andrew Sogokon and
                       Stefan Mitsch and
                       Yong Kiam Tan and
                       Katherine Cordwell and
                       Andr{\'{e}} Platzer},
          title     = {Pegasus: Sound Continuous Invariant Generation},
          journal   = {Form. Methods Syst. Des.},
          longjournal = {Formal Methods in System Design},
          year      = {},
          volume    = {},
          number    = {},
          pages     = {},
          doi       = {},
          issn      = {0925-9856},
          note      = {Special issue for selected papers from FM'19},
        }
    

        @INCOLLECTION{MitschP20,
          author    = {Stefan Mitsch and
                       Andr{\'{e}} Platzer},
          title     = {A Retrospective on Developing Hybrid Systems Provers
                       in the KeYmaera Family:
                       A Tale of Three Provers},
          booktitle = {Deductive Software Verification: Future Perspectives},
          pages     = {},
          year      = {2020},
          doi       = {10.1007/978-3-030-64354-6_2},
          editor    = {Wolfgang Ahrendt and
                       Richard Bubel and
                       Bernhard Beckert and
                       Reiner H{\"{a}}hnle and
                       Matthias Ulbrich},
          series    = {LNCS},
          volume    = {12345},
          publisher = {Springer},
          year      = {2020},
          isbn      = {},
          addresss  = {}
        }
    

        @inproceedings{DBLP:conf/fm/LunelMBT19,
          author    = {Simon Lunel and
                       Stefan Mitsch and
                       Beno{\^{\i}}t Boyer and
                       Jean{-}Pierre Talpin},
          title     = {Parallel Composition and Modular Verification of Computer Controlled
                       Systems in Differential Dynamic Logic},
          booktitle = {Formal Methods - The Next 30 Years - Third World Congress, {FM} 2019,
                       Porto, Portugal, October 7-11, 2019, Proceedings},
          pages     = {354--370},
          year      = {2019},
          crossref  = {DBLP:conf/fm/2019},
          url       = {https://doi.org/10.1007/978-3-030-30942-8\_22},
          doi       = {10.1007/978-3-030-30942-8\_22},
          timestamp = {Mon, 23 Sep 2019 13:52:37 +0200},
          biburl    = {https://dblp.org/rec/bib/conf/fm/LunelMBT19},
          bibsource = {dblp computer science bibliography, https://dblp.org}
        }
        @proceedings{DBLP:conf/fm/2019,
          editor    = {Maurice H. ter Beek and
                       Annabelle McIver and
                       Jos{\'{e}} N. Oliveira},
          title     = {Formal Methods - The Next 30 Years - Third World Congress, {FM} 2019,
                       Porto, Portugal, October 7-11, 2019, Proceedings},
          series    = {Lecture Notes in Computer Science},
          volume    = {11800},
          publisher = {Springer},
          year      = {2019},
          url       = {https://doi.org/10.1007/978-3-030-30942-8},
          doi       = {10.1007/978-3-030-30942-8},
          isbn      = {978-3-030-30941-1},
          timestamp = {Mon, 23 Sep 2019 13:47:30 +0200},
          biburl    = {https://dblp.org/rec/bib/conf/fm/2019},
          bibsource = {dblp computer science bibliography, https://dblp.org}
        }
    

        @inproceedings{DBLP:conf/fm/SogokonMTCP19,
          author    = {Andrew Sogokon and
                       Stefan Mitsch and
                       Yong Kiam Tan and
                       Katherine Cordwell and
                       Andr{\'{e}} Platzer},
          title     = {Pegasus: {A} Framework for Sound Continuous Invariant Generation},
          booktitle = {Formal Methods - The Next 30 Years - Third World Congress, {FM} 2019,
                       Porto, Portugal, October 7-11, 2019, Proceedings},
          pages     = {138--157},
          year      = {2019},
          crossref  = {DBLP:conf/fm/2019},
          url       = {https://doi.org/10.1007/978-3-030-30942-8\_10},
          doi       = {10.1007/978-3-030-30942-8\_10},
          timestamp = {Sat, 12 Oct 2019 12:51:42 +0200},
          biburl    = {https://dblp.org/rec/bib/conf/fm/SogokonMTCP19},
          bibsource = {dblp computer science bibliography, https://dblp.org}
        }
        @proceedings{DBLP:conf/fm/2019,
          editor    = {Maurice H. ter Beek and
                       Annabelle McIver and
                       Jos{\'{e}} N. Oliveira},
          title     = {Formal Methods - The Next 30 Years - Third World Congress, {FM} 2019,
                       Porto, Portugal, October 7-11, 2019, Proceedings},
          series    = {Lecture Notes in Computer Science},
          volume    = {11800},
          publisher = {Springer},
          year      = {2019},
          url       = {https://doi.org/10.1007/978-3-030-30942-8},
          doi       = {10.1007/978-3-030-30942-8},
          isbn      = {978-3-030-30941-1},
          timestamp = {Mon, 23 Sep 2019 13:47:30 +0200},
          biburl    = {https://dblp.org/rec/bib/conf/fm/2019},
          bibsource = {dblp computer science bibliography, https://dblp.org}
        }
    

        @article{DBLP:journals/ral/BohrerTMSP19,
          author    = {Rose Bohrer and
                       Yong Kiam Tan and
                       Stefan Mitsch and
                       Andrew Sogokon and
                       Andr{\'{e}} Platzer},
          title     = {A Formal Safety Net for Waypoint-Following in Ground Robots},
          journal   = {{IEEE} Robotics and Automation Letters},
          volume    = {4},
          number    = {3},
          pages     = {2910--2917},
          year      = {2019},
          url       = {https://doi.org/10.1109/LRA.2019.2923099},
          doi       = {10.1109/LRA.2019.2923099},
          timestamp = {Wed, 21 Aug 2019 08:33:57 +0200},
          biburl    = {https://dblp.org/rec/bib/journals/ral/BohrerTMSP19},
          bibsource = {dblp computer science bibliography, https://dblp.org}
        }
    

        @inproceedings{DBLP:conf/cpsweek/MitschSTJZWZ19,
          author    = {Stefan Mitsch and
                       Andrew Sogokon and
                       Yong Kiam Tan and
                       Xiangyu Jin and
                       Bohua Zhan and
                       Shuling Wang and
                       Naijun Zhan},
          title     = {{ARCH-COMP19} Category Report: Hybrid Systems Theorem Proving},
          booktitle = {{ARCH19.} 6th International Workshop on Applied Verification of Continuous
                       and Hybrid Systemsi, part of CPS-IoT Week 2019, Montreal, QC, Canada,
                       April 15, 2019.},
          pages     = {141--161},
          year      = {2019},
          crossref  = {DBLP:conf/cpsweek/2019arch},
          url       = {http://www.easychair.org/publications/paper/mSQ6},
          timestamp = {Wed, 03 Jul 2019 10:08:32 +0200},
          biburl    = {https://dblp.org/rec/bib/conf/cpsweek/MitschSTJZWZ19},
          bibsource = {dblp computer science bibliography, https://dblp.org}
        }
        @proceedings{DBLP:conf/cpsweek/2019arch,
          editor    = {Goran Frehse and
                       Matthias Althoff},
          title     = {{ARCH19.} 6th International Workshop on Applied Verification of Continuous
                       and Hybrid Systemsi, part of CPS-IoT Week 2019, Montreal, QC, Canada,
                       April 15, 2019},
          series    = {EPiC Series in Computing},
          volume    = {61},
          publisher = {EasyChair},
          year      = {2019},
          url       = {http://www.easychair.org/publications/volume/ARCH19},
          timestamp = {Wed, 03 Jul 2019 10:06:30 +0200},
          biburl    = {https://dblp.org/rec/bib/conf/cpsweek/2019arch},
          bibsource = {dblp computer science bibliography, https://dblp.org}
        }
    

            @INPROCEEDINGS{DBLP:conf/iccps/GarciaMP19,
              author    = {Luis Garcia and
                           Stefan Mitsch and
                           Andr{\'{e}} Platzer},
              title     = {{HyPLC}: Hybrid Programmable Logic Controller Program Translation for Verification},
              booktitle = {ICCPS},
              longbooktitle = {10th IEEE/ACM International Conference on Cyber-Physical Systems},
              year      = {2019},
              editor    = {Linda Bushnell and
                           Miroslav Pajic},
              pages     = {},
              publisher = {ACM},
              isbn      = {},
              doi       = {10.1145/3302509.3311036},
            }
        

            @INPROCEEDINGS{DBLP:conf/cyphy/MullerMSP18,
              author    = {Andreas M{\"{u}}ller and
                           Stefan Mitsch and
                           Wieland Schwinger and
                           Andr{\'{e}} Platzer},
              title     = {A Component-Based Hybrid Systems
                           Verification and Implementation Tool
                           in KeYmaera {X} (Tool Demonstration)},
              booktitle = {Cyber Physical Systems.
                           Model-Based Design - 8th International Workshop,
                           CyPhy 2018, and 14th International Workshop, {WESE} 2018, Turin, Italy,
                           October 4-5, 2018,
                           Revised Selected Papers},
              pages     = {91--110},
              year      = {2018},
              doi       = {10.1007/978-3-030-23703-5\_5},
              editor    = {Roger D. Chamberlain and
                           Walid Taha and
                           Martin T{\"{o}}rngren},
              series    = {LNCS},
              volume    = {11615},
              publisher = {Springer},
            }
        

            @ARTICLE{DBLP:journals/sttt/MullerMRSP18,
              author   = {Andreas M{\"{u}}ller and
                          Stefan Mitsch and
                          Werner Retschitzegger and
                          Wieland Schwinger and
                          Andr{\'{e}} Platzer},
              title     = {Tactical Contract Composition for Hybrid System Component Verification},
              journal   = {STTT},
              volume    = {20},
              number    = {6},
              year      = {2018},
              pages     = {615-643},
              note      = {Special issue for selected papers from FASE'17}
            }
        

            @INPROCEEDINGS{DBLP:conf/pldi/BohrerTMMP18,
              author    = {Rose Bohrer and
                           Yong Kiam Tan and
                           Stefan Mitsch and
                           Magnus O. Myreen and
                           Andr{\'{e}} Platzer},
              title     = {{VeriPhy}: Verified Controller Executables
                           from Verified Cyber-Physical System Models},
              pages     = {},
              year      = {2018},
              doi       = {},
              publisher = {{ACM}},
            }
        

            @ARTICLE{DBLP:journals/ijrr/MitschGVP17,
              author    = {Stefan Mitsch and
                           Khalil Ghorbal and
                           David Vogelbacher and
                           Andr{\'e} Platzer},
              title     = {Formal Verification of Obstacle Avoidance
                           and Navigation of Ground Robots},
              journal   = {I. J. Robotics Res.},
              longjournal={International Journal of Robotics Research},
              volume    = {36},
              number    = {12},
              pages     = {1312--1340},
              year      = {2017},
              doi       = {10.1177/0278364917733549},
              arXiv     = {1605.00604}
            }
        

            @inproceedings{DBLP:conf/cpsweek/0002MRSP17,
              author    = {Andreas M{\"{u}}ller and
                           Stefan Mitsch and
                           Werner Retschitzegger and
                           Wieland Schwinger and
                           Andr{\'{e}} Platzer},
              editor    = {Goran Frehse and
                           Matthias Althoff},
              title     = {A Benchmark for Component-based Hybrid Systems Safety Verification},
              booktitle = {{ARCH17.} 4th International Workshop on Applied Verification of Continuous
                           and Hybrid Systems, collocated with Cyber-Physical Systems Week (CPSWeek)
                           on April 17, 2017 in Pittsburgh, PA, {USA}},
              series    = {EPiC Series in Computing},
              volume    = {48},
              pages     = {65--74},
              publisher = {EasyChair},
              year      = {2017},
              url       = {https://easychair.org/publications/paper/DgT4},
              timestamp = {Wed, 27 May 2020 16:02:35 +0200},
              biburl    = {https://dblp.org/rec/conf/cpsweek/0002MRSP17.bib},
              bibsource = {dblp computer science bibliography, https://dblp.org}
            }
        

            @INPROCEEDINGS{DBLP:conf/rssrail/MitschGBGP17,
              author    = {Stefan Mitsch and
                           Marco Gario and
                           Christof J. Budnik and
                           Michael Golm and
                           Andr{\'e} Platzer},
              title     = {Formal Verification of Train Control with
                           Air Pressure Brakes},
              booktitle = {RSSRail},
              longbooktitle = {RSSRail 2017: Reliability, Safety,
                           and Security of Railway Systems},
              year      = {2017},
              pages     = {173-191},
              editor    = {Alessandro Fantechi and
                           Thierry Lecomte and
                           Alexander Romanovsky},
              volume    = {10598},
              doi       = {10.1007/978-3-319-68499-4_12},
              series    = {LNCS},
              publisher = {Springer},
            }
        

            @INPROCEEDINGS{DBLP:conf/fase/MullerMRSP17,
              author    = {Andreas M{\"u}ller and
                           Stefan Mitsch and
                           Werner Retschitzegger and
                           Wieland Schwinger and
                           Andr{\'e} Platzer},
              title     = {Change and Delay Contracts for
                           Hybrid System Component Verification},
              booktitle = {FASE},
              year      = {2017},
              pages     = {134-151},
              doi       = {10.1007/978-3-662-54494-5_8},
              editor    = {Marieke Huisman and
                           Julia Rubin},
              series    = {LNCS},
              volume    = {10202},
              publisher = {Springer},
            }
        

            @INPROCEEDINGS{DBLP:conf/itp/FultonMBP17,
              author    = {Nathan Fulton and
                           Stefan Mitsch and
                           Rose Bohrer and
                           Andr{\'e} Platzer},
              title     = {Bellerophon: Tactical Theorem Proving
                           for Hybrid Systems},
              booktitle = {ITP},
              longbooktitle = {Interactive Theorem Proving,
                           International Conference, ITP 2017},
              year      = {2017},
              pages     = {207-224},
              month     = {},
              doi       = {10.1007/978-3-319-66107-0_14},
              editor    = {Mauricio Ayala-Rinc{\'o}n and
                           C{\'e}sar A. Mu{\~n}oz},
              publisher = {Springer},
              series    = {LNCS},
              volume    = {10499},
              isbn      = {978-3-319-66106-3},
            }
        

            @INPROCEEDINGS{DBLP:conf/ifm/MullerMRSP16,
              author    = {Andreas M{\"u}ller and
                           Stefan Mitsch and
                           Werner Retschitzegger and
                           Wieland Schwinger and
                           Andr{\'e} Platzer},
              title     = {A Component-based Approach to
                           Hybrid Systems Safety Verification},
              booktitle = {IFM},
              longbooktitle={Integrated Formal Methods - 12th
                           International Conference, {IFM} 2016,
                           Reykjavik, Iceland, June 1-4, 2016, Proceedings},
              year      = {2016},
              pages     = {441-456},
              doi       = {10.1007/978-3-319-33693-0_28},
              editor    = {Erika Abraham and
                           Marieke Huisman},
              series    = {LNCS},
              volume    = {9681},
              publisher = {Springer},
              year      = {2016},
            }
        

            @ARTICLE{DBLP:journals/sttt/JeanninGKSGMP16,
              author    = {Jean{-}Baptiste Jeannin and
                           Khalil Ghorbal and
                           Yanni Kouskoulas and
                           Aurora Schmidt and
                           Ryan Gardner and
                           Stefan Mitsch and
                           Andr{\'e} Platzer},
              title     = {A Formally Verified Hybrid System for Safe Advisories in the
                           Next-generation Airborne Collision Avoidance System},
              journal   = {STTT},
              longjournal = {International Journal on Software Tools for Technology Transfer},
              year      = {2016},
              volume    = {19},
              number    = {6},
              pages     = {717--741},
              doi       = {10.1007/s10009-016-0434-1}
            }
        

            @ARTICLE{DBLP:journals/fmsd/MitschP16,
              author    = {Stefan Mitsch and
                           Andr{\'e} Platzer},
              title     = {{ModelPlex}: Verified Runtime Validation of
                           Verified Cyber-Physical System Models},
              journal   = {Form. Methods Syst. Des.},
              longjournal = {Formal Methods in System Design},
              year      = {2016},
              volume    = {49},
              number    = {1},
              pages     = {33-74},
              doi       = {10.1007/s10703-016-0241-z},
              issn      = {0925-9856},
              note      = {Special issue of selected papers from RV'14},
            }
        

    @inproceedings{DBLP:conf/itsc/0002MP15,
      author    = {Andreas M{\"{u}}ller and
                   Stefan Mitsch and
                   Andr{\'{e}} Platzer},
      title     = {Verified Traffic Networks: Component-Based Verification of Cyber-Physical
                   Flow Systems},
      booktitle = {{IEEE} 18th International Conference on Intelligent Transportation
                   Systems, {ITSC} 2015, Gran Canaria, Spain, September 15-18, 2015},
      pages     = {757--764},
      publisher = {{IEEE}},
      year      = {2015},
      url       = {https://doi.org/10.1109/ITSC.2015.128},
      doi       = {10.1109/ITSC.2015.128},
      timestamp = {Wed, 16 Oct 2019 14:14:57 +0200},
      biburl    = {https://dblp.org/rec/conf/itsc/0002MP15.bib},
      bibsource = {dblp computer science bibliography, https://dblp.org}
    }
    	

@article{DBLP:conf/cade/FultonMQVP15,
  author    = {Nathan Fulton and
               Stefan Mitsch and
               Jan-David Quesel and
               Marcus V{\"o}lp and
               Andr{\'e} Platzer},
  title     = {{KeYmaera X} - An Axiomatic Tactical Theorem Prover
               for Hybrid Systems},
  booktitle = {Automated Deduction - 25th International
               Conference, {CADE} 2015, Berlin, Germany,
               August 1-7, 2015. Proceedings},
  pages     = {527--538},
  year      = {2015},
  publisher = {Springer}
}
		

@article{DBLP:journals/csur/MitschPRS15,
  author    = {Stefan Mitsch and
               Andr{\'e} Platzer and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {Logic-based modeling approaches for qualitative
               and hybrid reasoning in dynamic spatial systems},
  journal   = {ACM Computing Surveys},
  year      = {2015},
  volume    = {48},
  number    = {1},
  pages     = {3:1--3:40},
}
		

@article{DBLP:journals/sttt/QueselMLAP15,
  author    = {Jan-David Quesel and
               Stefan Mitsch and
               Sarah Loos and
               Nikos Ar{\'e}chiga and
               Andr{\'e} Platzer},
  title     = {How to Model and Prove Hybrid Systems
               with {KeYmaera}: A Tutorial on Safety},
  journal   = {STTT},
  year      = {2015},
  volume    = {},
  number    = {},
  pages     = {},
}
		

@inproceedings{DBLP:conf/ksem/MullerMRS14,
  author    = {Andreas M{\"{u}}ller and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {A Conceptual Reference Model of Modeling and Verification Concepts
               for Hybrid Systems},
  booktitle = {Knowledge Science, Engineering and Management - 7th International
               Conference, {KSEM} 2014, Sibiu, Romania, October 16-18, 2014. Proceedings},
  pages     = {368--379},
  year      = {2014},
  crossref  = {DBLP:conf/ksem/2014},
  url       = {http://dx.doi.org/10.1007/978-3-319-12096-6_33},
  doi       = {10.1007/978-3-319-12096-6_33},
  timestamp = {Mon, 13 Oct 2014 13:57:55 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/ksem/MullerMRS14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/ksem/2014,
  editor    = {Robert Buchmann and
               Claudiu Vasile Kifor and
               Jian Yu},
  title     = {Knowledge Science, Engineering and Management - 7th International
               Conference, {KSEM} 2014, Sibiu, Romania, October 16-18, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8793},
  publisher = {Springer},
  year      = {2014},
  url       = {http://dx.doi.org/10.1007/978-3-319-12096-6},
  doi       = {10.1007/978-3-319-12096-6},
  isbn      = {978-3-319-12095-9},
  timestamp = {Mon, 13 Oct 2014 13:55:21 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/ksem/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
		

@inproceedings{DBLP:conf/rv/MitschP14,
  author    = {Stefan Mitsch and
               Andr{\'{e}} Platzer},
  title     = {ModelPlex: Verified Runtime Validation of Verified Cyber-Physical
               System Models},
  booktitle = {Runtime Verification - 5th International Conference, {RV} 2014, Toronto,
               ON, Canada, September 22-25, 2014. Proceedings},
  pages     = {199--214},
  year      = {2014},
  crossref  = {DBLP:conf/rv/2014},
  url       = {http://dx.doi.org/10.1007/978-3-319-11164-3_17},
  doi       = {10.1007/978-3-319-11164-3_17},
  timestamp = {Mon, 15 Sep 2014 11:23:13 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/rv/MitschP14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@proceedings{DBLP:conf/rv/2014,
  editor    = {Borzoo Bonakdarpour and
               Scott A. Smolka},
  title     = {Runtime Verification - 5th International Conference, {RV} 2014, Toronto,
               ON, Canada, September 22-25, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8734},
  publisher = {Springer},
  year      = {2014},
  url       = {http://dx.doi.org/10.1007/978-3-319-11164-3},
  doi       = {10.1007/978-3-319-11164-3},
  isbn      = {978-3-319-11163-6},
  timestamp = {Mon, 15 Sep 2014 11:21:34 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/rv/2014},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
		

@inproceedings{DBLP:conf/fm/MitschQP14,
  author    = {Stefan Mitsch and
               Jan-David Quesel and
               Andr{\'e} Platzer},
  title     = {Refactoring, Refinement, and Reasoning - A Logical Characterization
               for Hybrid Systems},
  booktitle = {FM},
  year      = {2014},
  pages     = {481-496},
  ee        = {http://dx.doi.org/10.1007/978-3-319-06410-9_33},
  crossref  = {DBLP:conf/fm/2014},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/fm/2014,
  editor    = {Cliff B. Jones and
               Pekka Pihlajasaari and
               Jun Sun},
  title     = {FM 2014: Formal Methods - 19th International Symposium,
               Singapore, May 12-16, 2014. Proceedings},
  booktitle = {FM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {8442},
  year      = {2014},
  isbn      = {978-3-319-06409-3},
  ee        = {http://dx.doi.org/10.1007/978-3-319-06410-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/apweb/MitschMRSS13,
  author    = {Stefan Mitsch and
               Andreas M{\"u}ller and
               Werner Retschitzegger and
               Andrea Salfinger and
               Wieland Schwinger},
  title     = {A Survey on Clustering Techniques for Situation Awareness},
  booktitle = {APWeb},
  year      = {2013},
  pages     = {815-826},
  ee        = {http://dx.doi.org/10.1007/978-3-642-37401-2_78},
  crossref  = {DBLP:conf/apweb/2013},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/apweb/2013,
  editor    = {Yoshiharu Ishikawa and
               Jianzhong Li and
               Wei Wang and
               Rui Zhang and
               Wenjie Zhang},
  title     = {Web Technologies and Applications - 15th Asia-Pacific Web
               Conference, APWeb 2013, Sydney, Australia, April 4-6, 2013.
               Proceedings},
  booktitle = {APWeb},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7808},
  year      = {2013},
  isbn      = {978-3-642-37400-5},
  ee        = {http://dx.doi.org/10.1007/978-3-642-37401-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/do-form/MitschPP13,
  author    = {Stefan Mitsch and
               Grant Olney Passmore and
               Andr{\'e} Platzer},
  title     = {A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems},
  booktitle = {Do-Form},
  year      = {2013},
  pages     = {8-17},
  crossref  = {DBLP:conf/do-form/2013},
}
@proceedings{DBLP:conf/do-form/2013,
  editor    = {Manfred Kerber and
               Christoph Lange and
               Colin Rowat},
  title     = {Enabling Domain Experts to use Formalised Reasoning - Symposium AISB,
               Do-Form 2013, Exeter, UK, April 3-5, 2013.
               Proceedings},
  booktitle = {Do-Form},
  publisher = {AISB},
  year      = {2013}
}
		

@inproceedings{DBLP:conf/iccps/MitschLP12,
  author    = {Stefan Mitsch and
               Sarah M. Loos and
               Andr{\'e} Platzer},
  title     = {Towards Formal Verification of Freeway Traffic Control},
  booktitle = {ICCPS},
  year      = {2012},
  pages     = {171-180},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/ICCPS.2012.25},
  crossref  = {DBLP:conf/iccps/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/iccps/2012,
  title     = {2012 IEEE/ACM Third International Conference on Cyber-Physical
               Systems, Beijing, China, April 17-19, 2012},
  booktitle = {ICCPS},
  publisher = {IEEE},
  year      = {2012},
  isbn      = {978-1-4673-1537-1},
  ee        = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6197284},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/www/WischenbartMKKPRSSWL12,
  author    = {Martin Wischenbart and
               Stefan Mitsch and
               Elisabeth Kapsammer and
               Angelika Kusel and
               Birgit Pr{\"o}ll and
               Werner Retschitzegger and
               Wieland Schwinger and
               Johannes Sch{\"o}nb{\"o}ck and
               Manuel Wimmer and
               Stephan Lechner},
  title     = {User profile integration made easy: model-driven extraction
               and transformation of social network schemas},
  booktitle = {WWW (Companion Volume)},
  year      = {2012},
  pages     = {939-948},
  ee        = {http://doi.acm.org/10.1145/2187980.2188227},
  crossref  = {DBLP:conf/www/2012c},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/www/2012c,
  editor    = {Alain Mille and
               Fabien L. Gandon and
               Jacques Misselis and
               Michael Rabinovich and
               Steffen Staab},
  title     = {Proceedings of the 21st World Wide Web Conference, WWW 2012,
               Lyon, France, April 16-20, 2012  (Companion Volume)},
  booktitle = {WWW (Companion Volume)},
  publisher = {ACM},
  year      = {2012},
  isbn      = {978-1-4503-1230-1},
  ee        = {http://dl.acm.org/citation.cfm?id=2187980},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/se/KuselMRSMS12,
  author    = {Angelika Kusel and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger and
               Ralph Mayr and
               Johannes Sch{\"o}nb{\"o}ck},
  title     = {Ontology-Driven Generation of Multi-View Modeling Tools},
  booktitle = {Software Engineering},
  publisher = {IASTED},
  year      = {2012},
  ee        = {http://dx.doi.org/10.2316/P.2012.780-007}
}
		

@inproceedings{DBLP:conf/its/BaumgartnerMMRSS12,
  author    = {Norbert Baumgartner and
               Stefan Mitsch and
               Andreas M{\"u}ller and
               Werner Retschitzegger and
               Andrea Salfinger and
               Wieland Schwinger},
  title     = {The Situation Radar – Visualizing Collaborative Situation Awareness in Traffic Control Systems},
  booktitle = {ITS World Congress},
  year      = {2012},
  ee        = {http://dx.doi.org/10.2316/P.2012.780-007}
}
		

@inproceedings{DBLP:conf/dasfaa/GottesheimMRSB11,
  author    = {Wolfgang Gottesheim and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger and
               Norbert Baumgartner},
  title     = {SemGen - Towards a Semantic Data Generator for Benchmarking
               Duplicate Detectors},
  booktitle = {DASFAA Workshops},
  year      = {2011},
  pages     = {490-501},
  ee        = {http://dx.doi.org/10.1007/978-3-642-20244-5_47},
  crossref  = {DBLP:conf/dasfaa/2011w},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/dasfaa/2011w,
  editor    = {Jianliang Xu and
               Ge Yu and
               Shuigeng Zhou and
               Rainer Unland},
  title     = {Database Systems for Adanced Applications - 16th International
               Conference, DASFAA 2011, International Workshops: GDB, SIM3,
               FlashDB, SNSMW, DaMEN, DQIS, Hong Kong, China, April 22-25,
               2011. Proceedings},
  booktitle = {DASFAA Workshops},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6637},
  year      = {2011},
  isbn      = {978-3-642-20243-8},
  ee        = {http://dx.doi.org/10.1007/978-3-642-20244-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/er/MitschRS11,
  author    = {Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {Towards Modeling Dynamic Behavior with Integrated Qualitative
               Spatial Relations},
  booktitle = {ER Workshops},
  year      = {2011},
  pages     = {271-280},
  ee        = {http://dx.doi.org/10.1007/978-3-642-24574-9_34},
  crossref  = {DBLP:conf/er/2011w},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/er/2011w,
  editor    = {Olga De Troyer and
               Claudia Bauzer Medeiros and
               Roland Billen and
               Pierre Hallot and
               Alkis Simitsis and
               Hans Van Mingroot},
  title     = {Advances in Conceptual Modeling. Recent Developments and
               New Directions - ER 2011 Workshops FP-UML, MoRE-BI, Onto-CoM,
               SeCoGIS, Variability@ER, WISM, Brussels, Belgium, October
               31 - November 3, 2011. Proceedings},
  booktitle = {ER Workshops},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6999},
  year      = {2011},
  isbn      = {978-3-642-24573-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-24574-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/ic3k/BaumgartnerGMRS11,
  author    = {Norbert Baumgartner and
               Wolfgang Gottesheim and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {Reasoning on Data Streams for Situation Awareness},
  booktitle = {KEOD},
  year      = {2011},
  pages     = {407-412},
  crossref  = {DBLP:conf/ic3k/2011keod},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ic3k/2011keod,
  editor    = {Joaquim Filipe and
               Jan L. G. Dietz},
  title     = {KEOD 2011 - Proceedings of the International Conference
               on Knowledge Engineering and Ontology Development, Paris,
               France, 26-29 October, 2011},
  booktitle = {KEOD},
  publisher = {SciTePress},
  year      = {2011},
  isbn      = {978-989-8425-80-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/iiwas/MitschGPPRSHRB11,
  author    = {Stefan Mitsch and
               Wolfgang Gottesheim and
               Franz Hermann Pommer and
               Birgit Pr{\"o}ll and
               Werner Retschitzegger and
               Wieland Schwinger and
               Robert Hutter and
               Gustavo Rossi and
               Norbert Baumgartner},
  title     = {Making workflows situation aware: an ontology-driven framework
               for dynamic spatial systems},
  booktitle = {iiWAS},
  year      = {2011},
  pages     = {182-188},
  ee        = {http://doi.acm.org/10.1145/2095536.2095568},
  crossref  = {DBLP:conf/iiwas/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/iiwas/2011,
  editor    = {David Taniar and
               Eric Pardede and
               Hong-Quang Nguyen and
               J. Wenny Rahayu and
               Ismail Khalil},
  title     = {iiWAS'2011 - The 13th International Conference on Information
               Integration and Web-based Applications and Services, 5-7
               December 2011, Ho Chi Minh City, Vietnam},
  booktitle = {iiWAS},
  publisher = {ACM},
  year      = {2011},
  isbn      = {978-1-4503-0784-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@INPROCEEDINGS{DBLP:conf/rss/MitschGP13,
  author    = {Stefan Mitsch and
               Khalil Ghorbal and
               Andr{\'e} Platzer},
  title     = {On Provably Safe Obstacle Avoidance for
               Autonomous Robotic Ground Vehicles},
  booktitle = {Robotics: Science and Systems},
  year      = {2013},
  editor    = {Paul Newman and Dieter Fox and David Hsu},
  longbooktitle = {Robotics: Science and Systems IX,
               Technical University of Berlin,
               Berlin, Germany, June 24-28, 2013},
  isbn      = {978-981-07-3937-9}
}
		

@INPROCEEDINGS{DBLP:conf/persdb/KapsammerLMPRSWW11,
  author    = {Elisabeth Kapsammer and
  			   Stephan Lechner and
  			   Stefan Mitsch and
               Birgit Pr{\"o}ll and
               Werner Retschitzegger and
               Wieland Schwinger and
               Manuel Wimmer and
               Martin Wischenbart},
  title     = {Towards a Reference Model for Social User Profiles: Concept {\&} Implementation},
  booktitle = {PersDB},
  publisher = {VLDB},
  year      = {2013},
  longbooktitle = {Personalized Access, Profile Management, and Context Awareness in Databases,
                   Seattle, WA, USA, September 2, 2011},
}
		

@inproceedings{DBLP:conf/er/BaumgartnerGMRS10,
  author    = {Norbert Baumgartner and
               Wolfgang Gottesheim and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {Situation Prediction Nets - Playing the Token Game for Ontology-Driven
               Situation Awareness},
  booktitle = {ER},
  year      = {2010},
  pages     = {202-218},
  ee        = {http://dx.doi.org/10.1007/978-3-642-16373-9_15},
  crossref  = {DBLP:conf/er/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/er/2010,
  editor    = {Jeffrey Parsons and
               Motoshi Saeki and
               Peretz Shoval and
               Carson C. Woo and
               Yair Wand},
  title     = {Conceptual Modeling - ER 2010, 29th International Conference
               on Conceptual Modeling, Vancouver, BC, Canada, November
               1-4, 2010. Proceedings},
  booktitle = {ER},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6412},
  year      = {2010},
  isbn      = {978-3-642-16372-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-16373-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/ic3k/GottesheimMRSB10,
  author    = {Wolfgang Gottesheim and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger and
               Norbert Baumgartner},
  title     = {WorkAware - Situation-aware Workflow Management},
  booktitle = {KMIS},
  year      = {2010},
  pages     = {246-252},
  crossref  = {DBLP:conf/ic3k/2010kmis},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ic3k/2010kmis,
  editor    = {Kecheng Liu and
               Joaquim Filipe},
  title     = {KMIS 2010 - Proceedings of the International Conference
               on Knowledge Management and Information Sharing, Valencia,
               Spain, October 25-28, 2010},
  booktitle = {KMIS},
  publisher = {SciTePress},
  year      = {2010},
  isbn      = {978-989-8425-30-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/otm/BaumgartnerGMRS10,
  author    = {Norbert Baumgartner and
               Wolfgang Gottesheim and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {Towards Duplicate Detection for Situation Awareness Based
               on Spatio-temporal Relations},
  booktitle = {OTM Conferences (2)},
  year      = {2010},
  pages     = {1097-1107},
  ee        = {http://dx.doi.org/10.1007/978-3-642-16949-6_31},
  crossref  = {DBLP:conf/otm/2010-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/otm/2010-2,
  editor    = {Robert Meersman and
               Tharam S. Dillon and
               Pilar Herrero},
  title     = {On the Move to Meaningful Internet Systems, OTM 2010 - Confederated
               International Conferences: CoopIS, IS, DOA and ODBASE, Hersonissos,
               Crete, Greece, October 25-29, 2010, Proceedings, Part II},
  booktitle = {OTM Conferences (2)},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6427},
  year      = {2010},
  isbn      = {978-3-642-16948-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-16949-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/qdb/BaumgartnerGMRS10,
  author    = {Norbert Baumgartner and
               Wolfgang Gottesheim and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {Improving Situation Awareness in Traffic Management},
  booktitle = {QDB},
  longbooktitle = {Quality in Databases. In conjunction with VLDB 2010,
                   September 13th, 2010, Singapore},
  year      = {2010},
  pages     = {5}
}
		

@inproceedings{DBLP:conf/bsn/KurschlMS09,
  author    = {Werner Kurschl and
               Stefan Mitsch and
               Johannes Sch{\"o}nb{\"o}ck},
  title     = {Modeling Distributed Signal Processing Applications},
  booktitle = {BSN},
  year      = {2009},
  pages     = {103-108},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/BSN.2009.20},
  crossref  = {DBLP:conf/bsn/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/bsn/2009,
  editor    = {Benny P. L. Lo and
               Paul Mitcheson},
  title     = {Sixth International Workshop on Wearable and Implantable
               Body Sensor Networks, BSN 2009, Berkeley, CA, USA, 3-5 June
               2009},
  booktitle = {BSN},
  publisher = {IEEE Computer Society},
  year      = {2009},
  isbn      = {978-0-7695-3644-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/itng/KurschlMS09,
  author    = {Werner Kurschl and
               Stefan Mitsch and
               Johannes Sch{\"o}nb{\"o}ck},
  title     = {Modeling Situation-Aware Ambient Assisted Living Systems
               for Eldercare},
  booktitle = {ITNG},
  year      = {2009},
  pages     = {1214-1219},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/ITNG.2009.25},
  crossref  = {DBLP:conf/itng/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/itng/2009,
  editor    = {Shahram Latifi},
  title     = {Sixth International Conference on Information Technology:
               New Generations, ITNG 2009, Las Vegas, Nevada, 27-29 April
               2009},
  booktitle = {ITNG},
  publisher = {IEEE Computer Society},
  year      = {2009},
  isbn      = {978-0-7695-3596-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/ksem/BaumgartnerGMRS09,
  author    = {Norbert Baumgartner and
               Wolfgang Gottesheim and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {On Optimization of Predictions in Ontology-Driven Situation
               Awareness},
  booktitle = {KSEM},
  year      = {2009},
  pages     = {297-309},
  ee        = {http://dx.doi.org/10.1007/978-3-642-10488-6_30},
  crossref  = {DBLP:conf/ksem/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/ksem/2009,
  editor    = {Dimitris Karagiannis and
               Zhi Jin},
  title     = {Knowledge Science, Engineering and Management, Third International
               Conference, KSEM 2009, Vienna, Austria, November 25-27,
               2009. Proceedings},
  booktitle = {KSEM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5914},
  year      = {2009},
  isbn      = {978-3-642-10487-9},
  ee        = {http://dx.doi.org/10.1007/978-3-642-10488-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/otm/BaumgartnerGMRS09,
  author    = {Norbert Baumgartner and
               Wolfgang Gottesheim and
               Stefan Mitsch and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {"Same, Same but Different" A Survey on Duplicate Detection
               Methods for Situation Awareness},
  booktitle = {OTM Conferences (2)},
  year      = {2009},
  pages     = {1050-1068},
  ee        = {http://dx.doi.org/10.1007/978-3-642-05151-7_22},
  crossref  = {DBLP:conf/otm/2009-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/otm/2009-2,
  editor    = {Robert Meersman and
               Tharam S. Dillon and
               Pilar Herrero},
  title     = {On the Move to Meaningful Internet Systems: OTM 2009, Confederated
               International Conferences, CoopIS, DOA, IS, and ODBASE 2009,
               Vilamoura, Portugal, November 1-6, 2009, Proceedings, Part
               II},
  booktitle = {OTM Conferences (2)},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5871},
  year      = {2009},
  isbn      = {978-3-642-05150-0},
  ee        = {http://dx.doi.org/10.1007/978-3-642-05151-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/broadcom/KurschlMS08,
  author    = {Werner Kurschl and
               Stefan Mitsch and
               Johannes Sch{\"o}nb{\"o}ck},
  title     = {An Engineering Toolbox to Build Situation Aware Ambient
               Assisted Living Systems},
  booktitle = {BroadCom},
  year      = {2008},
  pages     = {110-116},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/BROADCOM.2008.36},
  crossref  = {DBLP:conf/broadcom/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/broadcom/2008,
  editor    = {Johnson I. Agbinya and
               Elmarie Biermann and
               Yskandar Hamam and
               Ntsibane Ntlatlapa and
               Keith Ferguson},
  title     = {2008 Third International Conference on Broadband Communications,
               Information Technology {\&} Biomedical Applications, BroadCom
               2008, 23-26 November 2008, Pretoria, Gauteng, South Africa},
  booktitle = {BroadCom},
  publisher = {IEEE Computer Society},
  year      = {2008},
  isbn      = {978-0-7695-3453-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/icwn/KurschlGMPS08,
  author    = {Werner Kurschl and
               Wolfgang Gottesheim and
               Stefan Mitsch and
               Rene Prokop and
               Johannes Sch{\"o}nb{\"o}ck},
  title     = {Automatic Position Determination of Fixed Infrastructure
               Sensor Network Nodes based on Topology Sensing and Maps},
  booktitle = {ICWN},
  year      = {2008},
  pages     = {17-22},
  crossref  = {DBLP:conf/icwn/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icwn/2008,
  editor    = {Hamid R. Arabnia and
               Victor A. Clincy},
  title     = {Proceedings of the 2008 International Conference on Wireless
               Networks, July 14-17, 2008, Las Vegas, Nevada, USA},
  booktitle = {ICWN},
  publisher = {CSREA Press},
  year      = {2008},
  isbn      = {1-60132-091-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/iiwas/KurschlMSB08,
  author    = {Werner Kurschl and
               Stefan Mitsch and
               Johannes Sch{\"o}nb{\"o}ck and
               Wolfgang Beer},
  title     = {Modeling wireless sensor networks based context-aware emergency
               coordination systems},
  booktitle = {iiWAS},
  year      = {2008},
  pages     = {117-122},
  ee        = {http://doi.acm.org/10.1145/1497308.1497334},
  crossref  = {DBLP:conf/iiwas/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/iiwas/2008,
  editor    = {Gabriele Kotsis and
               David Taniar and
               Eric Pardede and
               Ismail Khalil Ibrahim},
  title     = {iiWAS'2008 - The Tenth International Conference on Information
               Integration and Web-based Applications Services, 24-26 November
               2008, Linz, Austria},
  booktitle = {iiWAS},
  publisher = {ACM},
  year      = {2008},
  isbn      = {978-1-60558-349-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/itng/KurschlGMPSB08,
  author    = {Werner Kurschl and
               Wolfgang Gottesheim and
               Stefan Mitsch and
               Rene Prokop and
               Johannes Sch{\"o}nb{\"o}ck and
               Wolfgang Beer},
  title     = {A Two-Layered Deployment Scheme for Wireless Sensor Network
               based Location Tracking},
  booktitle = {ITNG},
  year      = {2008},
  pages     = {726-730},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/ITNG.2008.164},
  crossref  = {DBLP:conf/itng/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/itng/2008,
  title     = {Fifth International Conference on Information Technology:
               New Generations (ITNG 2008), 7-8 April 2008, Las Vegas,
               Nevada, USA},
  booktitle = {ITNG},
  publisher = {IEEE Computer Society},
  year      = {2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/hicss/KurschlMPS07,
  author    = {Werner Kurschl and
               Stefan Mitsch and
               Rene Prokop and
               Johannes Sch{\"o}nb{\"o}ck},
  title     = {Gulliver-A Framework for Building Smart Speech-Based Applications},
  booktitle = {HICSS},
  year      = {2007},
  pages     = {30},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/HICSS.2007.243},
  crossref  = {DBLP:conf/hicss/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/hicss/2007,
  title     = {40th Hawaii International International Conference on Systems
               Science (HICSS-40 2007), CD-ROM / Abstracts Proceedings,
               3-6 January 2007,  Waikoloa, Big Island, HI, USA},
  booktitle = {HICSS},
  publisher = {IEEE Computer Society},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/icmb/KurschlGMPS07,
  author    = {Werner Kurschl and
               Wolfgang Gottesheim and
               Stefan Mitsch and
               Rene Prokop and
               Johannes Sch{\"o}nb{\"o}ck},
  title     = {Evaluation of a Mobile Multimodal Application Design - Major
               Usability Criteria and Usability Test Results},
  booktitle = {ICMB},
  year      = {2007},
  pages     = {68},
  crossref  = {DBLP:conf/icmb/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/icmb/2007,
  title     = {International Conference on Mobile Business (ICMB 2007),
               July 9-11, 2007, Toronto, Ontario, Canada},
  booktitle = {ICMB},
  publisher = {IEEE Computer Society},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/se/KurschlMPS07,
  author    = {Werner Kurschl and
               Stefan Mitsch and
               Rene Prokop and
               Johannes Sch{\"o}nb{\"o}ck},
  title     = {Development issues for speech-enabled mobile applications},
  booktitle = {Software Engineering},
  year      = {2007},
  pages     = {157-168},
  ee        = {http://subs.emis.de/LNI/Proceedings/Proceedings105/article1470.html},
  crossref  = {DBLP:conf/se/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/se/2007,
  editor    = {Wolf-Gideon Bleek and
               J{\"o}rg Raasch and
               Heinz Z{\"u}llighoven},
  title     = {Software Engineering 2007, Fachtagung des GI-Fachbereichs
               Softwaretechnik, 27.-30.3.2007 in Hamburg},
  booktitle = {Software Engineering},
  publisher = {GI},
  series    = {LNI},
  volume    = {105},
  year      = {2007},
  isbn      = {978-3-88579-199-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/itng/KurschlMP06,
  author    = {Werner Kurschl and
               Stefan Mitsch and
               Rene Prokop},
  title     = {SmartDOTS - A Framework for Efficient Data Synchronization
               on Mobile Devices},
  booktitle = {ITNG},
  year      = {2006},
  pages     = {300-305},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/ITNG.2006.124},
  crossref  = {DBLP:conf/itng/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/itng/2006,
  title     = {Third International Conference on Information Technology:
               New Generations (ITNG 2006), 10-12 April 2006, Las Vegas,
               Nevada, USA},
  booktitle = {ITNG},
  publisher = {IEEE Computer Society},
  year      = {2006},
  isbn      = {0-7695-2497-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/itng/KurschlMP06a,
  author    = {Werner Kurschl and
               Stefan Mitsch and
               Rene Prokop},
  title     = {SelectiveDES: A Distributed Event Service Add-On for Invocation-Based
               Middleware supporting Selective Multi-Channel Communication
               and Notification Delivery},
  booktitle = {ITNG},
  year      = {2006},
  pages     = {328-333},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/ITNG.2006.119},
  crossref  = {DBLP:conf/itng/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/itng/2006,
  title     = {Third International Conference on Information Technology:
               New Generations (ITNG 2006), 10-12 April 2006, Las Vegas,
               Nevada, USA},
  booktitle = {ITNG},
  publisher = {IEEE Computer Society},
  year      = {2006},
  isbn      = {0-7695-2497-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

@inproceedings{DBLP:conf/mms/KurschlMP06,
  author    = {Werner Kurschl and
               Stefan Mitsch and
               Rene Prokop},
  title     = {MobileWork Clearance Management - Challenges and Solutions},
  booktitle = {MMS},
  year      = {2006},
  pages     = {9-20},
  ee        = {http://subs.emis.de/LNI/Proceedings/Proceedings76/article4533.html},
  crossref  = {DBLP:conf/mms/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/mms/2006,
  editor    = {Thomas Kirste and
               Birgitta K{\"o}nig-Ries and
               Key Pousttchi and
               Klaus Turowski},
  title     = {Mobile Informationssysteme - Potentiale, Hindernisse, Einsatz,
               1. Fachtagung Mobilit{\"a}t und Mobile Informationssysteme
               (MMS), 20.-22. Februar 2006, Passau, Germany},
  booktitle = {MMS},
  publisher = {GI},
  series    = {LNI},
  volume    = {76},
  year      = {2006},
  isbn      = {3-88579-170-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		

Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

This paper introduces a uniform substitution calculus for dL-CHP, the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious prover kernels by using axioms instead of axiom schemata. Instantiations can be recovered from a single proof rule responsible for soundness-critical instantiation checks rather than being spread across axiom schemata in side conditions. Even though communication and parallelism reasoning are notorious for necessitating subtle soundness-critical side conditions, uniform substitution when generalized to dL-CHP manages to limit and isolate their conceptual overhead. Since uniform substitution has proven to simplify the implementation of hybrid systems provers substantially, uniform substitution for dL-CHP paves the way for a parsimonious implementation of theorem provers for hybrid systems with communication and parallelism.

Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars

Technology advances give us the hope of driving without human error, reducing vehicle emissions and simplifying an everyday task with the future of self-driving cars. Making sure these vehicles are safe is very important to the continuation of this field. In this paper, we formalize the Responsibility-Sensitive Safety model (RSS) for self-driving cars and prove the safety and optimality of this model in the longitudinal direction. We utilize the hybrid systems theorem prover KeYmaera X to formalize RSS as a hybrid system with its nondeterministic control choices and continuous motion model, and prove absence of collisions. We then illustrate the practicality of RSS through refinement proofs that turn the verified nondeterministic control envelopes into deterministic ones and further verified compilation to Python. The refinement and compilation are safety-preserving; as a result, safety proofs of the formal model transfer to the compiled code, while counterexamples discovered in testing the code of an unverified model transfer back. The resulting Python code allows to test the behavior of cars following the motion model of RSS in simulation, to measure agreement between the model and simulation with monitors that are derived from the formal model, and to report counterexamples from simulation back to the formal model.

Reward Shaping from Hybrid Systems Models in Reinforcement Learning

Reinforcement learning is increasingly often used as a learning technique to implement control tasks in autonomous systems. To meet stringent safety requirements, formal methods for learning-enabled systems, such as closed-loop neural network verification, shielding, falsification, and online reachability analysis, analyze learned controllers for safety violations. Besides filtering unsafe actions during training, these approaches view verification and training largely as separate tasks. We propose an approach based on logically constrained reinforcement learning to couple formal methods and reinforcement learning more tightly by generating safety-oriented aspects of reward functions from verified hybrid systems models. We demonstrate the approach on a standard reinforcement learning environment for longitudinal vehicle control.

Formal Artifacts as Explanations for System Correctness in Cyber-Physical Systems

Autonomous systems, such as self-driving cars and robots, are increasingly often entrusted with operating in safety-critical ways, which makes certification an important tool to ensure that systems are operating as intended. This paper argues that formal methods are a useful basis for certification not only in terms of their rigor, but also as a way of explaining evidence of system correctness at the right level of detail.

Implicit definitions with differential equations for KeYmaera X (System Description)

Definition packages in theorem provers provide users with means of defining and organizing concepts of interest. This system description presents a new definition package for the hybrid systems theorem prover KeYmaera X based on differential dynamic logic (dL). The package adds KeYmaera X support for user-defined smooth functions whose graphs can be implicitly characterized by dL formulas. Notably, this makes it possible to implicitly characterize functions, such as the exponential and trigonometric functions, as solutions of differential equations and then prove properties of those functions using dL's differential equation reasoning principles. Trustworthiness of the package is achieved by minimally extending KeYmaera X's soundness-critical kernel with a single axiom scheme that expands function occurrences with their implicit characterization. Users are provided with a high-level interface for defining functions and non-soundness-critical tactics that automate low-level reasoning over implicit characterizations in hybrid system proofs.

Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces

Automated train control improves railroad operation by safeguarding the motion of trains while increasing efficiency by enabling motion within a safe envelope. Train controllers decide when to slow trains down to avoid collisions with other trains on the track, stay inside movement authorities, and navigate slopes, curves and tunnels safely. These systems must base their decisions on detailed motion models to guarantee the absence of overshoot of the movement authority (safety) and limit undershoot (efficiency). This paper is the first to formally verify the safety of the Federal Railroad Administration freight train kinematics model with all its relevant forces and parameters, including track slope and curvature, air brake propagation, and resistive forces as computed by the Davis equation. Due to the significant competing influence of these parameters on train stopping distances, even designing train controllers is a nontrivial control challenge, which we solve using formal verification. For increased generality at reduced verification effort, we verify symbolic mathematical generalizations of the train control models and subsequently apply efficient uniform substitutions to obtain verification results for physical train control models.

Formally verified next-generation airborne collision avoidance games in ACAS X

The design of aircraft collision avoidance algorithms is a subtle but important challenge that merits the need for provable safety guarantees. Obtaining such guarantees is nontrivial given the unpredictability of the interplay of the intruder aircraft decisions, the ownship pilot reactions, and the subtlety of the continuous motion dynamics of aircraft. Existing collision avoidance systems, such as TCAS and the Next-Generation Airborne Collision Avoidance System ACAS X, have been analyzed assuming severe restrictions on the intruder's flight maneuvers, limiting their safety guarantees in real-world scenarios where the intruder may change its course.

This work takes a conceptually significant and practically relevant departure from existing ACAS X models by generalizing them to hybrid games with first-class representations of the ownship and intruder decisions coming from two independent players, enabling significantly advanced predictive power. By proving the existence of winning strategies for the resulting Adversarial ACAS X in differential game logic, collision-freedom is established for the rich encounters of ownship and intruder aircraft with independent decisions along differential equations for flight paths with evolving vertical/horizontal velocities. We present three classes of models of increasing complexity: single-advisory infinite-time models, bounded time models, and infinite time, multi-advisory models. Within each class of models, we identify symbolic conditions and prove that there then always is a possible ownship maneuver that will prevent a collision between the two aircraft.

A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.

Verifying Switched System Stability with Logic

Switched systems are known to exhibit subtle (in)stability behaviors requiring system designers to carefully analyze the stability of closed-loop systems that arise from their proposed switching control laws. This paper presents a formal approach for verifying switched system stability that blends classical ideas from the controls and verification literature using differential dynamic logic (dL), a logic for deductive verification of hybrid systems. From controls, we use standard stability notions for various classes of switching mechanisms and their corresponding Lyapunov function-based analysis techniques. From verification, we use dL's ability to verify quantified properties of hybrid systems and dL models of switched systems as looping hybrid programs whose stability can be formally specified and proven by finding appropriate loop invariants, i.e., properties that are preserved across each loop iteration. This blend of ideas enables a trustworthy implementation of switched system stability verification in the KeYmaera X prover based on dL. For standard classes of switching mechanisms, the implementation provides fully automated stability proofs, including searching for suitable Lyapunov functions. Moreover, the generality of the deductive approach also enables verification of switching control laws that require non-standard stability arguments through the design of loop invariants that suitably express specific intuitions behind those control laws. This flexibility is demonstrated on three case studies: a model for longitudinal flight control by Branicky, an automatic cruise controller, and Brockett's nonholonomic integrator.

Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned Systems

Machine learning is becoming increasingly important to con- trol the behavior of safety and financially critical components in sophis- ticated environments, where the inability to understand learned compo- nents in general, and neural nets in particular, poses serious obstacles to their adoption. Explainability and interpretability methods for learned systems have gained considerable academic attention, but the focus of current approaches on only one aspect of explanation, at a fixed level of abstraction, and limited if any formal guarantees, prevents those expla- nations from being digestible by the relevant stakeholders (e.g., end users, certification authorities, engineers) with their diverse backgrounds and situation-specific needs. We introduce Fanoos, a framework for combin- ing formal verification techniques, heuristic search, and user interaction to explore explanations at the desired level of granularity and fidelity. We demonstrate the ability of Fanoos to produce and adjust the abstractness of explanations in response to user requests on a learned controller for an inverted double pendulum and on a learned CPU usage model.

ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving

This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2021. The characteristic features of the HSTP category remain as in the previous editions [MST+18, MST+19, MMJ+20], it focuses on flexibility of programming languages as structuring principles for hybrid systems, unambiguity and precision of program semantics, and mathematical rigor of logical reasoning principles. The benchmark set includes nonlinear and parametric continuous and hybrid systems and hybrid games, each in three modes: fully automatic verification, semi-automatic verification from proof hints, proof checking from scripted tactics. This instance of the competition introduces extensions to the scripting language, a comparison of the influence of arithmetic backend versions on verification performance in KeYmaera X, as well as improvements in the HHL Prover.

Formally Verified Safety Net for Waypoint Navigation Neural Network Controllers

This paper describes a formal model of a "location, heading and speed" waypoint navigation task for an autonomous ground vehicle—that is, a task of navigating the vehicle towards a particular location so that it has the desired heading and speed when in that location. Our novel way of modeling this task makes formal reasoning over controller correctness tractable. We state our model in differential dynamic logic (dL), which we then use to establish a formal definition of waypoint feasibility and formally verify its validity in the KeYmaera X interactive theorem prover. The formal machine-checked proof witnesses that for any waypoint we consider feasible, the vehicle can indeed be controlled to reach it within the prescribed error bound. We also describe how we use these formal definitions and theorem statements to inform training of neural network controllers for performing this waypoint navigation task. Note that in our approach we do not need to rely on the neural network controller always being perfect—instead, the formal model allows a synthesis of a correct-by-construction safety net for the controller that checks whether the neural network output is safe to act upon and present a safe alternative if it is not.

Verified Quadratic Virtual Substitution for Real Arithmetic

This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The Tarski-Seidenberg theorem established that the first-order logic of real arithmetic is decidable by QE. However, in practice, QE algorithms are highly complicated and often combine multiple methods for performance. VS is a practically successful method for QE that targets formulas with low-degree polynomials. To our knowledge, this is the first work to formalize VS for quadratic real arithmetic including inequalities. The proofs necessitate various contributions to the existing multivariate polynomial libraries in Isabelle/HOL. Our framework is modularized and easily expandable (to facilitate integrating future optimizations), and could serve as a basis for developing practical general-purpose QE algorithms. Further, as our formalization is designed with practicality in mind, we export our development to SML and test the resulting code on 378 benchmarks from the literature, comparing to Redlog, Z3, Wolfram Engine, and SMT-RAT. This identified inconsistencies in some tools, underscoring the significance of a verified approach for the intricacies of real arithmetic.

Safe and Resilient Practical Waypoint-Following for Autonomous Vehicles

We combine theorem proving and reachability analysis for cyber-physical systems verification to arrive at a practical approach to safe waypoint-following for an autonomous mobile vehicle controlled by a learning-enabled controller. We propose a robust monitor verifying short-term and long-term safety simultaneously at runtime, thereby combining the benefits of both theorem proving and reachability analysis. The proposed novel monitor architecture allows temporary violation of long-term safety while maintaining short-term safety to recover to a state with long-term safety. The recovery is based on a fallback model predictive controller. The experiments conducted in a high-fidelity racing car simulator demonstrate that our framework is safe and resilient in path tracking scenarios, in which avoiding collision with the race track boundary and obstacles is required.

Implicit and Explicit Proof Management in KeYmaera X

Hybrid systems theorem proving provides strong correctness guarantees about the interacting discrete and continuous dynamics of cyber-physical systems. The trustworthiness of proofs rests on the soundness of the proof calculus and its correct implementation in a theorem prover. Correctness is easier to achieve with a soundness-critical core that is stripped to the bare minimum, but, as a consequence, proof convenience has to be regained outside the soundness-critical core with proof management techniques. We present modeling and proof management techniques that are built on top of the soundness-critical core of KeYmaeraX to enable expanding definitions, parametric proofs, lemmas, and other useful proof techniques in hybrid systems proofs. Our techniques steer the uniform substitution implementation of the differential dynamic logic proof calculus in KeYmaeraX to allow users choose when and how in a proof abstract formulas, terms, or programs become expanded to their concrete definitions, and when and how lemmas and sub-proofs are combined to a full proof. The same techniques are exploited in implicit sub-proofs (without making such sub-proofs explicit to the user) to provide proof features, such as temporarily hiding formulas, which are notoriously difficult to get right when implemented in the prover core, but become trustworthy as proof management techniques outside the core. We illustrate our approach with several useful proof techniques and discuss their presentation on the KeYmaeraX user interface.

Towards CPS Verification Engineering

While formal verification techniques are inevitable to ensure safety of critical cyber-phyical systems (CPS), engineering techniques to support the design and analysis of such CPS are still in their infancy. Therefore, we take a first step towards the provision of appropriate engineering techniques for CPS verification, by providing an extensive evaluation of the current state of the art, identifying challenges not yet tackled by existing approaches and by proposing a research roadmap intended to pave the way towards a fully supported engineering process for CPS verification models.

Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned Systems

Machine learning becomes increasingly important to control the behavior of safety and financially critical components in sophisticated environments, where the inability to understand learned compo- nents in general, and neural nets in particular, poses serious obstacles to their adoption. Explainabil- ity and interpretability methods for learned systems have gained considerable academic attention, but the focus of current approaches on only one as- pect of explanation, at a fixed level of abstraction, and limited if any formal guarantees, prevents those explanations from being digestible by the relevant stakeholders (e.g., end users, certification authori- ties, engineers) with their diverse backgrounds and situation-specific needs. We introduce Fanoos, a flexible framework for combining formal verifica- tion techniques, heuristic search, and user interac- tion to explore explanations at the desired level of granularity and fidelity. We demonstrate the ability of Fanoos to produce and adjust the abstractness of explanations in response to user requests on a learned controller for an inverted double pendulum and on a learned CPU usage model.

Pegasus: Sound continuous invariant generation

Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.

A Retrospective on Developing Hybrid System Provers in the KeYmaera Family: A Tale of Three Provers.

This chapter provides a retrospective on the developments of three theorem provers for hybrid systems. While all three theorem provers implement closely related logics of the family of differential dynamic logic, they pursue fundamentally different styles of theorem prover implementations. Since the three provers KeYmaera, KeYmaeraD, and KeYmaera X share a common core logic, yet no line of code, and differ vastly in prover implementation technology, their logical proximity yet technical distance enables us to draw conclusions about the various advantages and disadvantages of different prover implementation styles for different purposes, which we hope are of generalizable interest.

Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic

Computer-Controlled Systems (CCS) are a subclass of hybrid systems where the periodic relation of control components to time is paramount. Since they additionally are at the heart of many safety-critical devices, it is of primary importance to correctly model such systems and to ensure they function correctly according to safety requirements. Differential dynamic logic dL is a powerful logic to model hybrid systems and to prove their correctness. We contribute a component-based modeling and reasoning framework to dL that separates models into components with timing guarantees, such as reactivity of controllers and controllability of continuous dynamics. Components operate in parallel, with coarse-grained interleaving, periodic execution and communication. We present techniques to automate system safety proofs from isolated, modular, and possibly mechanized proofs of component properties parameterized with timing characteristics.

Pegasus: A Framework for Sound Continuous Invariant Generation

Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to automation of formal proofs of safety in hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.

A Formal Safety Net for Waypoint-Following in Ground Robots

We present a reusable formally verified safety net that provides end-to-end safety and liveness guarantees for two-dimensional waypoint-following of Dubins-type ground robots with tolerances and acceleration. First, we model a robot in differential dynamic logic and specify assumptions on the controller and robot kinematics. Second, we prove formal safety and liveness properties for waypoint-following with speed limits. Third, we synthesize a monitor, which is automatically proven to enforce model compliance at runtime. Fourth, our use of the VeriPhy toolchain makes these guarantees carry over down to the level of machine code with untrusted controllers, environments, and plans. The guarantees for the safety net apply to any robot as long as the waypoints are chosen safely and the physical assumptions in its model hold. Experiments show that these assumptions hold in practice, with an inherent tradeoff between compliance and performance.

ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving

This paper reports on the Hybrid Systems Theorem Proving (HSTP) category in the ARCH-COMP Friendly Competition 2019. The most important characteristic features of the HSTP category remain as in the previous edition [MST+18]: i) The flexibility of programming languages as structuring principles for hybrid systems, ii) The unambiguity and precision of program semantics, and iii) The mathematical rigor of logical reason- ing principles. The HSTP category especially features many nonlinear and parametric continuous and hybrid systems. Owing to the nature of theorem proving, HSTP again accommodates three modes: A) Automatic in which the entire verification is performed fully automatically without any additional input beyond the original hybrid system and its safety specification. H) Hints in which select proof hints are provided as part of the input problem specification, allowing users to communicate specific advice about the system such as loop invariants. S) Scripted in which a significant part of the verification is done with dedicated proof scripts or problem-specific proof tactics. This threefold split makes it possible to better identify the sources of scalability and efficiency bottlenecks in hybrid systems theorem proving. The existence of all three categories also makes it easier for new tools with a different focus to participate in the competition, wherever they focus on in the spectrum from fast proof checking all the way to full automation. The types of benchmarks considered and experimental findings are described in this paper as well.

HyPLC: Hybrid programmable logic controller program translation for verification

Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safety-critical industrial control systems. Formal verification provides ways of establishing correctness guarantees, which can be quite important for such safety-critical applications. But since PLC code does not include an analytic model of the system plant, their verification is limited to discrete properties. In this paper, we, thus, start the other way around with hybrid programs that include continuous plant models in addition to discrete control algorithms. Correctness properties of hybrid programs can be formally verified in the theorem prover KeYmaera X that implements differential dynamic logic, dL, for hybrid programs. After verifying the hybrid program, we now present an approach for translating hybrid programs into PLC code. The new HyPLC tool implements this translation of discrete control code of verified hybrid program models to PLC controller code and, vice versa, the translation of existing PLC code into the discrete control actions for a hybrid program given an additional input of the continuous dynamics of the system to be verified. This approach allows for the generation of real controller code while preserving, by compilation, the correctness of a valid and verified hybrid program. PLCs are common cyber-physical interfaces for safety-critical industrial control applications, and HyPLC serves as a pragmatic tool for bridging formal verification of complex cyber-physical systems at the algorithmic level of hybrid programs with the execution layer of concrete PLC implementations.

A component-based hybrid systems verification and implementation tool in KeYmaera X

Safety-critical cyber-physical systems (CPS) should be analyzed using formal verification techniques in order to gain insight into and obtain rigorous safety guarantees about their behavior. For practical purposes, methods are needed to split modeling and verification effort into manageable pieces and link formal artifacts and techniques with implementation. In this paper we present a tool chain that supports component-based modeling and verification of CPS, generation of monitors, and systematic (but unverified) translation of models and monitors into executable code. A running example demonstrates how to model a system in a component-based fashion in differential dynamic logic (dL), how to represent and structure these models in the syntax of the hybrid systems theorem prover KeYmaera X (which implements dL), and how to prove properties in KeYmaera X. The verified components are the source for translation into executable C code, which can be run on controlled components (e.g., a robot). Additionally, we demonstrate how to generate monitors that validate the behavior of uncontrolled components (e.g., validate the assumptions made about obstacles)

Tactical contract composition for hybrid system component verification

We present an approach for hybrid systems that combines the advantages of component-based modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Component-based modeling can be used to split large models into multiple component models with local responsibilities to reduce modeling complexity. Yet, this only helps the analysis if verification proceeds one component at a time. In order to benefit from the decomposition of a system into components for both modeling and verification purposes, we prove that the safety of compatible components implies safety of the composed system. We implement our composition theorem as a tactic in the KeYmaera X theorem prover, allowing automatic generation of a KeYmaera X proof for the composite system from proofs for the components without soundness-critical changes to KeYmaera X. Our approach supports component contracts (i.e., input assumptions and output guarantees for each component) that characterize the magnitude and rate of change of values exchanged between components. These contracts can take into account what has changed between two components in a given amount of time since the last exchange of information.

VeriPhy: Verified controller executables from verified cyber-physical models

We present VeriPhy, a verified pipeline which automatically transforms verified high-level models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic (dL) to verified controller executables. VeriPhy proves that all safety results are preserved end-to-end as it bridges abstraction gaps, including: i) the gap between mathematical reals in physical models and machine arithmetic in the implementation ii) the gap between real physics and its differential-equation models iii) and the gap between nondeterministic controller models and machine code. VeriPhy reduces CPS safety to the faithfulness of the physical environment, which is checked at runtime by synthesized, verified monitors. We use three provers in this effort: KeYmaera X, HOL4, and Isabelle/HOL. To minimize the trusted base, we cross-verify KeYmaera X in Isabelle/HOL. We evaluate the resulting controller and monitors on commodity robotics hardware.

At scale, formal verification of hybrid systems is challenging, but a potential remedy is the observation that systems often come with a number of natural components with certain local responsibilities. Ideally, such a compartmentalization into more manageable components also translates to hybrid systems verification, so that safety properties about the whole system can be derived from local verification results. We propose a benchmark consisting of a sequence of three case studies, where components interact to achieve system safety. The baseline for the benchmark is the verification effort from a monolithic fashion (i.e., the entire system without splitting it into components). We describe how to split the system models used in these case studies into components with local responsibilities, and what is expected about their interaction to guarantee system safety. The benchmark can be used to assess the performance, automation, and verification features of component-based verification approaches.

Formal verification of train control with air pressure brakes

Train control technology enhances the safety and efficiency of railroad operation by safeguarding the motion of trains to prevent them from leaving designated areas of operation and colliding with other trains. It is crucial for safety that the trains engage their brakes early enough in order to make sure they never leave the safe part of the track. Efficiency considerations, however, also require that the train does not brake too soon, which would limit operational suitability. It is surprisingly subtle to reach the right tradeoffs and identify the right control conditions that guarantee safe motion without being overly conservative. In pursuit of an answer, we develop a hybrid system model with discrete control decisions for acceleration, brakes, and with continuous differential equations for their physical effects on the motion of the train. The resulting hybrid system model is systematically derived from the Federal Railway Administration model for flat terrain by conservatively neglecting minor forces. The main contribution of this paper is the identification of a controller with control constraints that we formally verify to always guarantee collision freedom in the FRA model. The safe braking behavior of a train is influenced not only by the train configuration (e.g., train length and mass), but also by physical characteristics (e.g., brake pressure propagation and reaction time). We formalize train control safety properties in differential dynamic logic and prove the correctness of the train control models in the theorem prover KeYmaera X.

Change and delay contracts for hybrid system component verification

In this paper, we present reasoning techniques for a component-based modeling and verification approach for hybrid systems comprising discrete dynamics as well as continuous dynamics, in which the components have local responsibilities. Our approach supports component contracts (i.e., input assumptions and output guarantees of interfaces) that are more general than previous component-based hybrid systems verification techniques in the following ways: We introduce change contracts, which characterize how current values exchanged between components along ports relate to previous values. We also introduce delay contracts, which describe the change relative to the time that has passed since the last value was exchanged. Together, these contracts can take into account what has changed between two components in a given amount of time since the last exchange of information. Most crucially, we prove that the safety of compatible components implies safety of the composite. The proof steps of the theorem are also implemented as a tactic in KeYmaera X, allowing automatic generation of a KeYmaera X proof for the composite system from proofs of the concrete components.

Bellerophon: Tactical theorem proving for hybrid systems

Hybrid systems combine discrete and continuous dynamics, which makes them attractive as models for systems that combine computer control with physical motion. Verification is undecidable for hybrid systems and challenging for many models and properties of practical interest. Thus, human interaction and insight are essential for verification. Interactive theorem provers seek to increase user productivity by allowing them to focus on those insights. We present a tactics language and library for hybrid systems verification, named Bellerophon, that provides a way to convey insights by programming hybrid systems proofs. We demonstrate that in focusing on the important domain of hybrid systems verification, Bellerophon emerges with unique automation that provides a productive proving experience for hybrid systems from a small foundational prover core in the KeYmaera X prover. Among the automation that emerges are tactics for decomposing hybrid systems, discovering and establishing invariants of nonlinear continuous systems, arithmetic simplifications to maximize the benefit of automated solvers and general-purpose heuristic proof search. Our presentation begins with syntax and semantics for the Bellerophon tactic combinator language, culminating in an example verification effort exploiting Bellerophon's support for invariant and arithmetic reasoning for a non-solvable system.

Formal verification of obstacle avoidance and navigation of ground robots

This article answers fundamental safety questions for ground robot navigation: Under which circumstances does which control decision make a ground robot safely avoid obstacles? Unsurprisingly, the answer depends on the exact formulation of the safety objective as well as the physical capabilities and limitations of the robot and the obstacles. Because uncertainties about the exact future behavior of a robot's environment make this a challenging problem, we formally verify corresponding controllers and provide rigorous safety proofs justifying why they can never collide with the obstacle in the respective physical model. To account for ground robots in which different physical phenomena are important, we analyze a series of increasingly strong properties of controllers for increasingly rich dynamics and identify the impact that the additional model parameters have on the required safety margins. We analyze and formally verify: (i) static safety, which ensures that no collisions can happen with stationary obstacles, (ii) passive safety, which ensures that no collisions can happen with stationary or moving obstacles while the robot moves, (iii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well, and (iv) passive orientation safety, which allows for imperfect sensor coverage of the robot, i.e., the robot is aware that not everything in its environment will be visible. We formally prove that safety can be guaranteed despite sensor uncertainty and actuator perturbation. We complement these provably correct safety properties with liveness properties: we prove that provably safe motion is flexible enough to let the robot navigate waypoints and pass intersections. In order to account for the mixed influence of discrete control decisions and the continuous physical motion of the ground robot, we develop corresponding hybrid system models and use differential dynamic logic theorem proving techniques to formally verify their correctness. Since these models identify a broad range of conditions under which control decisions are provably safe, our results apply to any control algorithm for ground robots with the same dynamics. As a demonstration, we, thus, also synthesize provably correct runtime monitor conditions that check the compliance of any control algorithm with the verified control decisions.

A component-based approach to hybrid systems safety verification

We study a component-based approach to simplify the challenges of verifying large-scale hybrid systems. Component-based modeling can be used to split large models into partial models to reduce modeling complexity. Yet, verification results also need to transfer from components to composites. In this paper, we propose a component-based hybrid system verification approach that combines the advantages of component-based modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Our strategy is to decompose the system into components, verify their local safety individually and compose them to form an overall system that provably satisfies a global contract, without proving the whole system. We introduce the necessary formalism to define the structure and behavior of components and a technique how to compose components such that safety properties provably emerge from component safety.

A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system

The Next-Generation Airborne Collision Avoidance System (ACAS X) is intended to be installed on all large aircraft to give advice to pilots and prevent mid-air collisions with other aircraft. It is currently being developed by the Federal Aviation Administration (FAA). In this paper we determine the geometric configurations under which the advice given by ACAS X is safe under a precise set of assumptions and formally verify these configurations using hybrid systems theorem proving techniques. We consider subsequent advisories and show how to adapt our formal verification to take them into account. We examine the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal hybrid systems proving approaches are helping to ensure the safety of ACAS X. Our approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.

ModelPlex: Verified runtime validation of verified cyber-physical system models

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.

Verified Traffic Networks: Component-Based Verification of Cyber-Physical Flow Systems

We address the problem how high-fidelity verification results about the hybrid systems dynamics of cyber-physical flow systems can be provided at the scale of large (traffic) networks without prohibitive analytic cost. We propose the use of contracts for traffic flow components concisely capturing the conditions for a safe operation in the context of a traffic network. This reduces the analysis of flows in the full traffic network to simple arithmetic checks of the local compatibility of the traffic component contracts, while retaining higher-fidelity correctness guarantees of the global hybrid systems models that inherits from correct contracts of the hybrid system components. We evaluate our approach in a case study of a modular traffic network and a prototypical implementation in a model-based analysis and design tool for traffic flow networks.

KeYmaera X - An Axiomatic Tactical Theorem Prover for Hybrid Systems

KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems. Reasoning about complicated hybrid systems models requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute these tactics in parallel, and interface with partial proofs via an extensible user interface.
Advanced proof search features—and user-defined tactics in particular—are difficult to check for soundness. To admit extension and experimentation in proof search without reducing trust in the prover, KeYmaera X is built up from a small trusted kernel. The prover kernel contains a list of sound dL axioms that are instantiated using a uniform substitution proof rule. Isolating all soundness-critical reasoning to this prover kernel obviates the intractable task of ensuring that each new proof search algorithm is implemented correctly. Preliminary experiments suggest that a single layer of tactics on top of the prover kernel provides a rich language for implementing novel and sophisticated proof search techniques.

Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems

Autonomous agents that operate as components of dynamic spatial systems are becoming increasingly popular and mainstream. Applications can be found in consumer robotics, in road, rail, and air transportation, manufacturing, and military operations. Unfortunately, the approaches to modeling and analyzing the behavior of dynamic spatial systems are just as diverse as these application domains. In this paper, we discuss reasoning approaches for the medium-term control of autonomous agents in dynamic spatial systems, which requires a sufficiently detailed description of the agent's behavior and environment, but may still be conducted in a qualitative manner. We survey logic-based qualitative and hybrid modeling and commonsense reasoning approaches w.r.t. their features for describing and analyzing dynamic spatial systems in general, and the actions of autonomous agents operating therein in particular. We introduce a conceptual reference model, which summarizes the current understanding of the characteristics of dynamic spatial systems based on a catalog of evaluation criteria derived from the model. We assess the modeling features provided by logic-based qualitative commonsense and hybrid approaches for projection, planning, simulation, and verification of dynamic spatial systems. We provide a comparative summary of the modeling features, discuss lessons learned, and introduce a research roadmap for integrating different approaches of dynamic spatial system analysis to achieve coverage of all required features.

How to model and prove hybrid systems with KeYmaera: A tutorial on safety

This paper is a tutorial on how to model hybrid systems as hybrid programs in differential dynamic logic and how to prove complex properties about these complex hybrid systems in KeYmaera, an automatic and interactive formal verification tool for hybrid systems. Hybrid systems can model highly nontrivial controllers of physical plants, whose behaviors are often safety critical such as trains, cars, airplanes, or medical devices. Formal methods can help design systems that work correctly. This paper illustrates how KeYmaera can be used to systematically model, validate, and verify hybrid systems. We develop tutorial examples that illustrate challenges arising in many real-world systems. In the context of this tutorial, we identify the impact that modeling decisions have on the suitability of the model for verification purposes. We show how the interactive features of KeYmaera can help users understand their system designs better and prove complex properties for which the automatic prover of KeYmaera still takes an impractical amount of time. We hope this paper is a helpful resource for designers of embedded and cyber-physical systems and that it illustrates how to master common practical challenges in hybrid systems verification.

A Conceptual Reference Model of Modeling and Verification Concepts for Hybrid Systems

Cyber-physical systems (CPS), which are computerized systems directly interfacing their real-world surroundings, leverage the construction of increasingly autonomous systems. To meet the high safety demands of CPS, verification of their behavior is crucial, which has led to a wide range of tools for modeling and verification of hybrid systems. These tools are often used in combination, because they employ a wide range of different formalisms for modeling, and aim at distinct verification goals and techniques. To manage and exchange knowledge in the verification process and to overcome a lack of a common classification, we unify different terminologies and concepts of a variety of modeling and verification tools in a conceptual reference model (CRM). Furthermore, we illustrate how the CRM can support comparing models and propose future extension.

ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models

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 w.r.t. the model. Otherwise, all bets are off. This paper 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. Model- Plex ensures 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, assuming the system dynamics deviation is bounded. 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. This paper, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic.

From Safety to Guilty and From Liveness to Niceness

Robots are solving challenging tasks that we want them to be able to perform (liveness), but we also do not want them to endanger their surroundings (safety). Formal methods provide ways of proving such correctness properties, but have the habit of only saying “yes” when the answer is “yes” (soundness). More often than not, formal methods say “no”: They find out that the system is neither safe nor live, because there are “unexpected” circumstances in which the robot just cannot do what we expect it to. Inspecting those unexpected circumstances is informative, and identifies constraints on reasonable behavior of the environment. This ultimately leads from safety to the question of who is guilty depending on whose action caused the safety violation. It also leads from liveness to the question of what behavior of the environment is nice enough so that the robot can finish its task.

Collaborative Verification-Driven Engineering of Hybrid Systems

Hybrid systems with both discrete and continuous dynamics are an important model for real-world cyber-physical systems. The key challenge is to ensure their correct functioning w.r.t. safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-defined and traceable manner, and formal verification to prove their correctness. Their combination forms the vision of verification-driven engineering. Often, hybrid systems are rather complex in that they require expertise from many domains (e.g., robotics, control systems, computer science, software engineering, and mechanical engineering). Moreover, despite the remarkable progress in automating formal verification of hybrid systems, the construction of proofs of complex systems often requires nontrivial human guidance, since hybrid systems verification tools solve undecidable problems. It is, thus, not uncommon for development and verification teams to consist of many players with diverse expertise. This paper introduces a verification-driven engineering toolset that extends our previous work on hybrid and arithmetic verification with tools for (i) graphical (UML) and textual modeling of hybrid systems, (ii) exchanging and comparing models and proofs, and (iii) managing verification tasks. This toolset makes it easier to tackle large-scale verification tasks.

Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems

Refactoring of code is a common device in software engineering. As cyber-physical systems (CPS) become ever more complex, similar engineering practices become more common in CPS development. Proper safe developments of CPS designs are accompanied by a proof of correctness. Since the inherent complexities of CPS practically mandate iterative development, frequent changes of models are standard practice, but require reverication of the resulting models after every change. To overcome this issue, we develop proof-aware refactorings for CPS. That is, we study model transformations on CPS and show how they correspond to relations on correctness proofs. As the main technical device, we show how the impact of model transformations on correctness can be characterized by dierent notions of renement in dierential dynamic logic. Furthermore, we demonstrate the application of renements on a series of safety-preserving and liveness-preserving refactorings. For some of these we can give strong results by proving on a meta-level that they are correct. Where this is impossible, we construct proof obligations for showing that the refactoring respects the renement relation.

On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles

Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. We formally study two safety properties of avoiding both stationary and moving obstacles: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and theorem proving techniques that describe and formally verify the robot’s discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty.

A Tour of BeAware: A Situation Awareness Framework for Control Centers

Large control centers, as needed in road traffic, typically manage highly dynamic environments. They process vast amounts of information from heterogeneous data sources about a large number of real-world objects, which are anchored in time and space. In such systems, human operators are vulnerable to information overload and, thus, may fail to be aware of the overall meaning of available information and its implications. With BeAware, we propose a software framework that supports the development of situation awareness applications for control centers. The contribution of this paper is twofold: First, we integrate existing ontologies with spatio-temporal reasoning concepts, focusing on extensibility. We introduce meta-modeling concepts that allow us to assess and project situations and actions using semantic web technology. Second, we compare the runtime performance of the situation comprehension capabilities of a generic, ontology-driven implementation and a domain-specific relational-database-backed implementation, and discuss the strengths and shortcomings of each approach.

BeAware! Situation awareness, the ontology-driven way

Information overload is a severe problem for human operators of large-scale control systems as, for example, encountered in the domain of road traffic management. Operators of such systems are at risk to lack situation awareness, because existing systems focus on the mere presentation of the available information on graphical user interfaces—thus endangering the timely and correct identification, resolution, and prevention of critical situations. In recent years, ontology-based approaches to situation awareness featuring a semantically richer knowledge model have emerged. However, current approaches are either highly domain-specific or have, in case they are domain-independent, shortcomings regarding their reusability.
In this paper, we present our experience gained from the development of BeAware!, a framework for ontology-driven information systems aiming at increasing an operator's situation awareness. In contrast to existing domain-independent approaches, BeAware!'s ontology introduces the concept of spatio-temporal primitive relations between observed real-world objects thereby improving the reusability of the framework. To show its applicability, a prototype of BeAware! has been implemented in the domain of road traffic management. An overview of this prototype and lessons learned for the development of ontology-driven information systems complete our contribution.

A Survey on Clustering Techniques for Situation Awareness

Situation awareness (SAW) systems aim at supporting assessment of critical situations as, e.g., needed in traffic control centers, in order to reduce the massive information overload. When assessing situations in such control centers, SAW systems have to cope with a large number of heterogeneous but interrelated real-world objects stemming from various sources, which evolve over time and space. These specific requirements harden the selection of adequate data mining techniques, such as clustering, complementing situation assessment through a data-driven approach by facilitating configuration of the critical situations to be monitored. Thus, this paper aims at presenting a survey on clustering approaches suitable for SAW systems. As a prerequisite for a systematic comparison, criteria are derived reflecting the specific requirements of SAW systems and clustering techniques. These criteria are employed in order to evaluate a carefully selected set of clustering approaches, summarizing the approaches’ strengths and shortcomings.

A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems

Hybrid systems with both discrete and continuous dynamics are an important model for real-world physical systems. The key challenge is how to ensure their correct functioning w.r.t. safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-dened and traceable manner, and formal verication to prove their correctness. Their combination forms the vision of verication-driven engineering. Despite the remarkable progress in automating formal verication of hybrid systems, the construction of proofs of complex systems often requires signicant human guidance, since hybrid systems verication tools solve undecidable problems. It is thus not uncommon for verication teams to consist of many players with diverse expertise. This paper introduces a verication-driven engineering toolset that extends our previous work on hybrid and arithmetic verication with tools for (i) modeling hybrid systems, (ii) exchanging and comparing models and proofs, and (iii) managing verication tasks. This toolset makes it easier to tackle large-scale verication tasks.

Towards Formal Verification of Freeway Traffic Control

We study how CPS technology can help improve freeway traffic by combining local car GPS positioning, traffic center control decisions, and communication to achieve more tightly coupled feedback control in intelligent speed adaptation. We develop models for an intelligent speed adaptation that respects variable speed limit control and incident management. We identify safe ranges for crucial design parameters in these systems and, using the theorem prover KeYmaera, formally verify safety of the resulting CPS models. Finally, we show how those parameter ranges can be used to decide trade-offs for practical system implementations even for design parameters that are not modeled formally.

User profile integration made easy: model-driven extraction and transformation of social network schemas

User profile integration from multiple social networks is indispensable for gaining a comprehensive view on users. Although current social networks provide access to user profile data via dedicated APIs, they fail to provide accurate schema information, which aggravates the integration of user profiles, and not least the adaptation of applications in the face of schema evolution. To alleviate these problems, this paper presents, firstly, a semi-automatic approach to extract schema information from instance data. Secondly, transformations of the derived schemas to different technical spaces are utilized, thereby allowing, amongst other benefits, the application of established integration tools and methods. Finally, as a case study, schemas are derived for Facebook, Google+, and LinkedIn. The resulting schemas are analyzed (i) for completeness and correctness according to the documentation, and (ii) for semantic overlaps and heterogeneities amongst each other, building the basis for future user profile integration.

Ontology-Driven Generation of Multi-View Modeling Tools

Multi-view modeling allows viewing and modifying models at different levels of abstraction and from different viewpoints, thus circumventing drawbacks of modeling tools used in isolation. Although state-of-the-art frameworks for developing modeling tools are recently being increasingly integrated, the development of multi-view modeling tools still demands the integration of modeling artifacts expressed using various notations from different frameworks, resulting in high development effort. In order to reduce this effort, we propose to automatically derive such modeling tool artifacts from ontologies which, due to their semantically rich representation of domain knowledge, can capture the necessary information using a single notation, such as OWL. To this end, we describe a mapping from OWL to Ecore, which is tailored to building multiview modeling tools based upon the Eclipse platform. We complement our contributions with several lessons learned while building such a multi-view modeling tool.

The Situation Radar – Visualizing Collaborative Situation Awareness in Traffic Control Systems

Today, traffic control responsibilities are split among different authorities that operate on a shared environment. Since each authority may have its own restrained views of the environment, collaboration is crucial to better resolve critical traffic situations. As a consequence, traffic control operators have to establish collaborative situation awareness (SA), i.e., they have to correctly judge the meaning and impact of information in their own control center, as well as to keep track of the information status and needs of other operators, their planned and executed actions, and further important details of collaboration. In this paper we discuss requirements on a user interface for collaborative SA. We adapt well-practiced visualization patterns to propose the Situation Radar, a user interface element aiming at establishing collaborative SA in traffic control.

SemGen - Towards a Semantic Data Generator for Benchmarking Duplicate Detectors

Benchmarking the quality of duplicate detection methods requires comprehensive knowledge on duplicate pairs in addition to sufficient size and variability of test data sets. While extending real-world data sets with artificially created data is promising, current approaches to such synthetic data generation, however, work solely on a quantitative level, which entails that duplicate semantics are only implicitly represented, leading to only insufficiently configurable variability.
In this paper we propose SemGen, a semantics-driven approach to synthetic data generation. SemGen first diversifies real-world objects on a qualitative level, before in a second step quantitative values are generated. To demonstrate the applicability of SemGen, we propose how to define duplicate semantics for the domain of road traffic management. A discussion of lessons learned concludes the paper.

Towards Modeling Dynamic Behavior with Integrated Qualitative Spatial Relations

Situation awareness and geographic information systems in dynamic spatial systems such as road traffic management (RTM) aim to detect and predict critical situations on the basis of relations between entities. Such relations are described by qualitative calculi, each of them focusing on a certain aspect (e.g., topology). Since these calculi are defined isolated from each other, dependencies between then are not explicitly modeled. We argue, that a taxonomy—containing a plethora of special cases of inter-calculi dependencies—can only be defined in a consistent manner, if evolution of entities and the relations of calculi are grounded in a unified model. In this paper, we define such a unified model, which is used to derive a taxonomy of inter-calculi dependency constraints contained in an ontology utilizing various spatial calculi. The applicability of this approach is demonstrated with a case study in RTM, and concluded with lessons learned from a prototypical implementation.

Reasoning on Data Streams for Situation Awareness

Information overload is a severe problem for human operators of large-scale control systems, for instance, in road traffic management. In order to determine a complete and coherent view of the overall situation (i. e., gain situation awareness), an operator of such a system must consider various heterogeneous sources providing streams of information about a large number of real-world objects. Since the usage of ontologies has been regarded to be beneficial for achieving situation awareness, various ontology-driven situation awareness systems have been proposed. Coping with evolving and volatile individuals in ontologies, however, has not been their focus up to now. In this paper, we describe how concepts from data stream management systems and stream reasoning, such as sliding windows, continuous queries, and incremental reasoning, can be adjusted to support reasoning over highly dynamic ontologies for situation awareness. We conclude our paper with a prototypical implementation and a discussion of lessons learned, pointing to directions of future work.

Making workflows situation aware: an ontology-driven framework for dynamic spatial systems

Business processes face constantly changing context factors like varying customer behavior or market conditions that force to adapt the underlying workflows to these evolving situations. Information overload induced by the diversity of context factors, however, leads to the inability to provide coherently modeled, comprehensible, and re-usable workflows and the failure to recognize relevant situations in time. The main goal of our research project ProFlow is to leverage situation awareness in all phases of workflow management especially focusing on dynamic spatial systems as encountered, e.g., in the domain of road traffic management. ProFlow thereby bases on a generic ontology-driven framework for situation perception and comprehension. This paper details on the corresponding ontological representations especially addressing extension points that allow developers to extend and configure our framework for their own application domains. This forms the basis for the overall system architecture, which is laid out along its prototypical implementation.

Towards a Reference Model for Social User Profiles: Concept & Implementation

Despite the recent spreading of social networks, which leads to scattered social user profile information, current user models hardly incorporate social aspects. In addition, user models are often heterogenous with respect to focus and coverage. A comprehensive view on social user profiles, however, would be required, for instance, for building sophisticated recommender systems, or to provide users with means to control disclosure and usage of their integrated profile data. Therefore, we encountered the need for a reference model, which can serve as a basis for developing more specialized models and facilitate communication among stakeholders. In this paper we present such a reference model for social user profiles, which is extensible as well as comprehensive. The proposed model provides a generic core for extensions, and a comprehensive set of concrete concepts from existing social networks and user models, as well as concepts to represent meta information. In addition, a first prototypical implementation in terms of an ontology in OWL is discussed.

Situation Prediction Nets - Playing the Token Game for Ontology-Driven Situation Awareness

Situation awareness in large-scale control systems such as road traffic management aims to predict critical situations on the basis of spatio-temporal relations between real-world objects. Such relations are described by domain-independent calculi, each of them focusing on a certain aspect, for example topology. The fact that these calculi are described independently of the involved objects, isolated from each other, and irrespective of the distances between relations leads to inaccurate and crude predictions. To improve the overall quality of prediction while keeping the modeling effort feasible, we propose a domain-independent approach based on Colored Petri Nets that complements our ontology-driven situation awareness framework BeAware!. These Situation Prediction Nets can be generated automatically and allow increasing (i) prediction precision by exploiting ontological knowledge in terms of object characteristics and interdependencies between relations and (ii) increasing expressiveness by associating multiple distance descriptions with transitions. The applicability of Situation Prediction Nets is demonstrated using real-world traffic data.

WorkAware - Situation-aware Workflow Management

Business processes face constantly changing context factors like varying customer behavior or market conditions that force to adapt the underlying workflows to these evolving situations. Information overload induced by the diversity of context factors, however, leads to the inability to provide coherently modeled, comprehensible, and re-usable workflows, the failure to recognize relevant situations in time, and finally, the lack of provenance information urgently needed for optimizing workflows. The main goal of our research project WorkAware is to leverage situation awareness in all phases of business process management. WorkAware will be based on a generic ontology-driven framework for situation perception, comprehension and projection and will employ aspect-oriented techniques for achieving extensible workflow models and tracking of provenance information.

Towards Duplicate Detection for Situation Awareness Based on Spatio-temporal Relations

Systems supporting situation awareness typically integrate information about a large number of real-world objects anchored in time and space provided by multiple sources. These sources are often characterized by identical, incomplete, and even contradictory information. Because of that, duplicate detection methods are of paramount importance, allowing to explore whether or not information concerns one and the same real-world object. Although many such duplicate detection methods exist, a recent survey revealed that the characteristics of situation awareness—highly dynamic and vague information, which is often available in qualitative form only—are not supported sufficiently well. This paper proposes concepts for qualitative duplicate detection to cope with these key issues of situation awareness based on spatio-temporal relations between objects.

Improving Situation Awareness in Traffic Management

Information overload is a severe problem for operators of large-scale control systems, as such systems typically provide a vast amount of information about a large number of real-world objects. Systems supporting situation awareness have recently gained attention as way to help operators to grasp the overall meaning of available information. To fulfill this task, data quality has to be ensured by assessment and improvement strategies. In this paper, a vision towards a methodology for data quality assessment and improvement for situation awareness systems is presented.

Modeling Distributed Signal Processing Applications

Wireless Sensor Networks in general and Body Sensor Networks in particular enable sophisticated applications in pervasive healthcare, sports training and other domains, where interconnected nodes work together. Their main goal is to derive context from raw sensor data with feature extraction and classification algorithms. Body sensor networks not only comprise a single sensor type or family but demand different hardware platforms, e.g., sensors to measure acceleration or blood-pressure, or tiny mobile devices to communicate with the user. The problem arises how to efficiently deal with these heterogeneous platforms and programming languages. This paper presents a distributed signal processing framework based on TinyOS and nesC. The framework forms the basis for a Model-Driven Software Development approach. By raising the level of abstraction formal models hide implementation specifics of the framework in a Platform Specific Model. A Platform Independent Model further lifts modeling to functional and non-functional requirements independent from platforms. Thereby we promote cooperation between domain experts and software engineers and facilitate reusability of applications across different platforms.

Modeling Situation-Aware Ambient Assisted Living Systems for Eldercare

The development of ambient assisted living (AAL) systems, which are tailored to health or elder care, requires specific methods and tools. AAL systems make often use of wireless sensor networks, machine learning algorithms and sensory devices. Since wireless sensor networks and their sensors are inhomogeneous, it became apparent that such systems need to cope with different hardware platforms, different programming languages, unreliable wireless communication, energy constraints, data analysis algorithms, recognition of situations, and deployment options. Developers to date tend to use a bottom-up approach: hardware components dictate the development of AAL systems and thereby restrict the range of use cases that can be realized; domain experts by contrast would prefer a top-down approach and model the system’s functionality independently from the hardware platform. Currently available software development environments and tools do not adequately support domain experts and developers to accomplish these tasks efficiently. This paper presents methods that support domain experts in their top-down approach, as well as technically experienced developers in their bottom-up approach. The implemented tools enable a model-driven software development process (from platform-independent modeling to generating AAL application code) and thus facilitate programming AAL systems.

On Optimization of Predictions in Ontology-Driven Situation Awareness

Systems supporting situation awareness in large-scale control systems, such as, e.g., encountered in the domain of road traffic management, pursue the vision of allowing human operators prevent critical situations. Recently, approaches have been proposed, which express situations, their constituting objects, and the relations in-between (e.g., road works causing a traffic jam), by means of domain-independent ontologies, allowing automatic prediction of future situations on basis of relation derivation. The resulting vast search space, however, could lead to unacceptable runtime performance and limited expressiveness of predictions. In this paper, we argue that both issues can be remedied by taking inherent characteristics of objects into account. For this, an ontology is proposed together with optimization rules, allowing to exploit such characteristics for optimizing predictions. A case study in the domain of road traffic management reveals that search space can be substantially reduced for many real-world situation evolutions, and thereby demonstrates the applicability of our approach.

"Same, Same but Different" A Survey on Duplicate Detection Methods for Situation Awareness

Systems supporting situation awareness typically deal with a vast stream of information about a large number of real-world objects anchored in time and space provided by multiple sources. These sources are often characterized by frequent updates, heterogeneous formats and most crucial, identical, incomplete and often even contradictory information. In this respect, duplicate detection methods are of paramount importance allowing to explore whether or not information having, e.g., different origins or different observation times concern one and the same real-world object. Although many such duplicate detection methods have been proposed in literature—each of them having different origins, pursuing different goals and often, by nature, being heavily domain-specific—the unique characteristics of situation awareness and their implications on the method’s applicability were not the focus up to now. This paper examines existing duplicate detection methods appearing to be suitable in the area of situation awareness and identifies their strengths and shortcomings. As a prerequisite, based on a motivating case study in the domain of road traffic management, an evaluation framework is suggested, which categorizes the major requirements on duplicate detection methods with regard to situation awareness.

An Engineering Toolbox to Build Situation Aware Ambient Assisted Living Systems

Due to increasing anticipated average life and health expenditure ambient assisted living (AAL) systems attract the attention of researchers. To successfully build and deploy AAL systems knowledge from different fields of computer science is needed: pervasive computing to gain the raw data, machine learning and pattern recognition to interpret these data and HCI knowledge to allow implicit interaction with the system. In this paper we propose a reference architecture for building AAL systems. Based on this reference architecturewe introduce a toolbox that simplifies the development of AAL systems. The toolbox consists of a meta-model for pipeline systems, a low-level context model, high-level context ontologies, customizable components and tool support.

Automatic Position Determination of Fixed Infrastructure Sensor Network Nodes based on Topology Sensing and Maps

The tracking of objects and humans has recently received a lot of attention as a tool to improve business processes, occupational and public safety. In industrial environments wireless sensor networks can facilitate deployment of tracking applications as they can establish a standalone communication infrastructure (a so called mesh network). Many such positioning and location tracking systems deploy a fixed infrastructure (so-called beacons) with known positions to determine the position of mobile nodes in the network. For large-scale deployments the installation effort of such systems may be a major cost-factor, as the exact position of each beacon needs to be manually determined and associated with map material. We therefore propose a position determination tool that automatically finds the positions of beacons based on the sensor network’s topology, digital map material of the environment, and a small set of anchor nodes.

Modeling wireless sensor networks based context-aware emergency coordination systems

Current research on context information focuses on the use of new kinds of sensors and on the aggregation and interpretation of sensor data. Having a closer look at applications supporting emergency scenarios with context information several problems arise. Emergency activities are complex coordination tasks which involve a multitude of different roles and resources. The definition of emergency scenarios and the mapping of relevant context information is a time-consuming and error-prone task.
This work discusses how a model-based approach can support the definition of emergency scenarios at an abstract level. The abstract representation (PIM, Platform Independent Model) of an activity is then transformed into a platform-specific model (PSM), which includes a collection of context sensors. We show that the use of a model-based approach simplifies the definition of complex context-sensitive applications, and how this increases the flexibility to use different sensor platforms in different emergency scenarios.

A Two-Layered Deployment Scheme for Wireless Sensor Network based Location Tracking

The tracking of objects and humans has recently received a lot of attention as a tool to improve business processes, occupational, and public safety. In wireless sensor networks location information is needed to put sensor readings into geographical context. In industrial environments wireless sensor networks can facilitate deployment of tracking applications as they can establish a standalone communication infrastructure (so called mesh networks). Nevertheless the communication infrastructure and thus the tracking applications rely on radio transmission. Therefore problems like ambiguous locations and the neighboring-room problem known from other radio-based tracking solutions may occur. We propose a two layered deployment scheme for wireless sensor networks to overcome these limitations. It consists of a robust communication layer and a flexible location layer, which enable per room accuracy. Such accuracy is sufficient for many types of tracking applications.

Gulliver-A Framework for Building Smart Speech-Based Applications

Speech recognition has matured over the past years to the point that companies can seriously consider its use. However, from a developer?s perspective we observe that speech input is rarely used in mobile application development, not even if it allowed users to work with their devices more flexibly. This stems partly from the fact that programming speech-enabled applications is tedious, because there is insufficient framework and tool support.
This paper describes a component-based framework that uniformly supports development of multimodal applications on heterogeneous devices, ranging from laptop PCs to mobile phones. It especially focuses on distributed components (each performing a single step in speech recognition) to enable speech recognition on any type of device. Moreover, it describes how to develop and integrate different user interfaces for one application (voice-only, graphical-only, and multimodal) in a model-driven development approach, to minimize development and maintenance costs.

Evaluation of a Mobile Multimodal Application Design - Major Usability Criteria and Usability Test Results

Mobile broadband internet access and powerful mobile devices make interesting and novel communication applications possible (e.g., recently emerging VoIP applications). Additionally, speech recognition has matured to the point that companies can seriously consider its use. We developed a distributed framework that enables multimodal user interfaces with speech recognition (dictation and command/control) on any type of mobile device. But do users already accept speech as additional input modality, and if so, which usability challenges arise when developing multimodal applications? This paper presents the results from usability tests that we conducted with a mobile multimodal e-mail and contact application. Based on the results we point out major usability criteria that need to be met in developing mobile multimodal applications.

Development issues for speech-enabled mobile applications

Developing a speech-based application for mobile devices requires work upfront, since mobile devices and speech recognition systems vary dramatically in their capabilities. While mobile devices can concisely be classified by their processing power, memory, operating system and wireless network speed it is a bit trickier for speech recognition engines. This paper presents a comprehensive approach that comprises a profound classification of speech recognition systems for mobile applications and a framework for mobile and distributed speech recognition. The framework called Gulliver speeds up the development process with multi-modal components that can be easily used in a GUI designer and with abstraction layers that support the integration of various speech recognition engines depending on the user's needs. The framework itself provides the base for a model-driven development approach.

SmartDOTS - A Framework for Efficient Data Synchronization on Mobile Devices

Mobile enterprise applications typically access data from the enterprise's various applications. Allowing the mobile application to access these data online only would be a major hindrance for mobile workers that cannot assume a constantly available network connection. We present a middleware called Smart Data Off The Spot (SmartDOTS) for building nomadic distributed enterprise applications. In SmartDOTS, the business data model is represented per device, network, and task; this representation configures SmartDOTS to provide business data tailored to the specific capabilities (e.g., memory capacity) of a device, and needs of a task. The SmartDOTS approach is independent of persistent storages; it is part of the application developer?s task to provide server-side persistency. Thus, any (legacy) application can be integrated with SmartDOTS.

SelectiveDES: A Distributed Event Service Add-On for Invocation-Based Middleware supporting Selective Multi-Channel Communication and Notification Delivery

Mobile enterprise applications typically access data from the enterprise's various applications to support collaborative working processes. Allowing the mobile application to access these data online only would be a major hindrance for mobile workers that cannot assume a constantly available network connection. This problem can be handled by middleware systems, which provide a way to prefetch data on the mobile device. But changes and events on the central data cannot be foreseen; moreover, they cannot be delivered to disconnected mobile clients. We introduce a distributed event service named SelectiveDES for managing and delivering events to mobile clients in unpredictable network environments. SelectiveDES is designed as an addon to common invocation-based middleware systems; it is based on the publish-subscribe paradigm and supports selective multi-channel communication and notification delivery.

Mobile Work Clearance Management - Challenges and Solutions

We present a system called MOSES, which is a mobile work clearance management system for complex and large-area industrial machines. Based on an extensive field study of current work clearance practices, we identified important challenges and developed several solutions. MOSES shows how an enterprise application, like an enterprise resource planning system, can be extended to improve occupational safety for maintenance personnel. The presented solution consists of a work clearance management extension for several existing enterprise resource planning systems and a mobile work clearance management for mobile devices. The paper also describes a framework called Smart Data Off The Spot (SmartDOTS) for building nomadic distributed enterprise applications that supports data replication and synchronization from various enterprise applications. The framework allows the modelling of business data, so that device-, network and task-specific data replication, and context-dependent network selection can be modelled and automatically be executed by the SmartDOTS framework. This paper shows the design and implementation of a prototypical mobile work clearance system, which uses the SmartDOTS approach.

Application Development and Management of Smart Camera Networks

This chapter focuses on the management and the application development of distributed smart camera systems by observing the more general point of view of embedded sensor networks. The proposed approach relies on a model-based software engineering concept which allows a more unified and simplified design. Basically, the model-based system development concept provides high-level system functions and facilities for generating platform-specific code. This chapter outlines how this framework allows the integration of models at different levels, e.g., for exploiting low-level sensor data as well as high-level knowledge-based models for detection, classification, and representation of high-level situations in specific use cases. The usefulness of the presented approach shall be demonstrated in a real-world scenario targeting safety and security surveillance in a public airport environment.

Model-Driven Prototyping Support for Pervasive Healthcare Applications

Pervasive healthcare applications aim at improving habitability by assisting individuals in living autonomously. To achieve this goal, data on an individual’s behavior and his or her environment (often collected with wireless sensors) is interpreted by machine learning algorithms; their decision finally leads to the initiation of appropriate actions, e.g., turning on the light. Developers of pervasive healthcare applications therefore face complexity stemming, amongst others, from different types of environmental and vital parameters, heterogeneous sensor platforms, unreliable network connections, as well as from different programming languages. Moreover, developing such applications often includes extensive prototyping work to collect large amounts of training data to optimize the machine learning algorithms. In this chapter the authors present a model-driven prototyping approach for the development of pervasive healthcare applications to leverage the complexity incurred in developing prototypes and applications. They support the approach with a development environment that simplifies application development with graphical editors, code generators, and pre-defined components.