×
            @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    = {},
              number    = {},
              pages     = {},
              year      = {2017},
              doi       = {10.1177/0278364917733549},
              arXiv     = {1605.00604}
            }
        
            @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    = {},
              number    = {},
              pages     = {},
              doi       = {10.1007/s10009-016-0434-1},
              url       = {http://www.cs.cmu.edu/~aplatzer/pub/acasx-zones-long.pdf}
            }
        
            @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},
            }
        
@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{,
  author    = {Stefan Mitsch and
               Jan-David Quesel and
               Andr{\'e} Platzer},
  title     = {From Safety to Guilty and from Liveness to Niceness},
  booktitle = {5th Workshop on Formal Methods for Robotics and Automation},
  year      = {2014}
}
		
×
@article{DBLP:journals/mics/MitschPP14,
  author    = {Stefan Mitsch and
               Grant Olney Passmore and
               Andr{\'e} Platzer},
  title     = {Collaborative Verification-Driven Engineering of Hybrid
               Systems},
  journal   = {Mathematics in Computer Science},
  volume    = {8},
  number    = {1},
  year      = {2014},
  pages     = {71-97},
  ee        = {http://dx.doi.org/10.1007/s11786-014-0176-y},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
		
×
@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}
}		
		
×
@article{DBLP:journals/if/BaumgartnerMMSRS14,
  author    = {Norbert Baumgartner and
               Stefan Mitsch and
               Andreas M{\"u}ller and
               Andrea Salfinger and
               Werner Retschitzegger and
               Wieland Schwinger},
  title     = {A Tour of {BeAware}: A Situation Awareness Framework 
               for Control Centers},
  journal   = {Information Fusion},
  volume    = {20},
  number    = {},
  year      = {2014},
  pages     = {155-173},
  ee        = {http://dx.doi.org/10.1016/j.inffus.2014.01.008},
  bibsource = {}
}
  		
×
@article{DBLP:journals/dke/BaumgartnerGMRS10,
  author    = {Norbert Baumgartner and
        	     Wolfgang Gottesheim and
                 Stefan Mitsch and
               	 Werner Retschitzegger and
                 Wieland Schwinger},
  title     = {{BeAware!} - Situation awareness, the ontology-driven way},
  journal   = {Data Knowl. Eng.},
  volume    = {69},
  number    = {11},
  year      = {2010},
  pages     = {1181-1193},
  ee        = {http://dx.doi.org/10.1016/j.datak.2010.07.008},
  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}
}		
		
×

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 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.

×

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 di erent notions of re nement in di erential 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 pro les, 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 pro les, 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.

×

Book Contributions

Werner Kurschl, Stefan Mitsch, Johannes Schönböck.
Model-Driven Prototyping Support for Pervasive Healthcare Applications,
In Pervasive and Smart Technologies for Healthcare, IGI Global, 2010.
[ bib | abstract | doi ]

Wolfgang Beer, Bernhard Moser, Werner Kurschl, Stefan Mitsch, Florian Matusek, Stephan Sutor.
Application Development and Management of Smart Camera Networks,
In Smart Cameras, Springer, 2009.
[ bib | abstract | doi ]

Journal Publications

Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer.
Formal verification of obstacle avoidance and navigation of ground robots. International Journal of Robotics Research,, To appear.
[ pdf | bib | abstract | doi ]

Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, and André Platzer.
A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. STTT, 2016. Special issue for selected papers from TACAS'15.
[ pdf | bib | abstract | doi ]

Stefan Mitsch, Andre Platzer
ModelPlex: Verified runtime validation of verified cyber-physical system models. Formal Methods in System Design, 49(1), pp. 33-74. 2016. Special issue for selected papers from RV'14.
[ pdf | bib | abstract | doi ]

Stefan Mitsch, Andre Platzer, Werner Retschitzegger, Wieland Schwinger.
Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems. Computing Surveys, ACM, 2015.
[ pdf | bib | abstract | doi ]

Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Arechiga, Andre Platzer.
How to model and prove hybrid systems with KeYmaera: A tutorial on safety. STTT, Springer, 2015.
[ pdf | bib | abstract | doi ]

Stefan Mitsch, Grant Olney Passmore, Andre Platzer.
Collaborative Verification-Driven Engineering of Hybrid Systems. J. Mathematics in Computer Science, Springer, 8(1):71-97, 2014.
[ pdf | bib | abstract | arXiv | doi ]

Norbert Baumgartner, Stefan Mitsch, Andreas Müller, Andrea Salfinger, Werner Retschitzegger, Wieland Schwinger.
A Tour of BeAware: A Situation Awareness Framework for Control Centers. J. Information Fusion, Elsevier, 20(2014):155-173, 2014.
[ pdf | bib | abstract | doi ]

Norbert Baumgartner, Wolfgang Gottesheim, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger.
BeAware!—Situation Awareness, the Ontology-Driven Way. J. Data and Knowledge Engineering, Elsevier, 69(11):1181-1193, 2010.
[ pdf | bib | abstract | poster | doi ]

Conference Publications

Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer.
KeYmaera X - An Axiomatic Tactical Theorem Prover for Hybrid Systems In CADE 2015.
[ pdf | bib | abstract | doi ]

Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger.
A Conceptual Reference Model of Modeling and Verification Concepts for Hybrid Systems In KSEM 2014.
[ bib | abstract | doi ]

Stefan Mitsch, André Platzer.
ModelPlex: Verified Runtime Validation of Verified Cyber-Physical System Models. In RV 2014.
[ pdf | bib | abstract | report | slides | study | doi ]

Stefan Mitsch, Jan-David Quesel, André Platzer.
From Safety to Guilty and from Liveness to Niceness. In Formal Methods for Robotics and Automation 2014.
[ pdf | bib | abstract ]

Stefan Mitsch, Jan-David Quesel, André Platzer.
Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems. In FM 2014.
[ pdf | bib | abstract | slides ]

Stefan Mitsch, Khalil Ghorbal, André Platzer.
On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles. In RSS 2013.
[ pdf | bib | abstract | poster | slides | video | study | Sphinx Project ]

Stefan Mitsch, Andreas Müller, Werner Retschitzegger, Andrea Salfinger, Wieland Schwinger.
A Survey on Clustering Techniques for Situation Awareness. In APWeb 2013: 815-826. Springer 2013.
[ pdf | bib | abstract | doi ]

Stefan Mitsch, Grant Olney Passmore, André Platzer.
A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems. In Do-Form 2013: 8-17. AISB 2013.
[ pdf | bib | abstract ]

Stefan Mitsch, Sarah M. Loos, André Platzer.
Towards Formal Verification of Freeway Traffic Control. In ICCPS 2012: 171-180. ACM/IEEE 2012.
[ pdf | bib | abstract | doi | slides | study | Sphinx Project ]

Martin Wischenbart, Stefan Mitsch, Elisabeth Kapsammer, Angelika Kusel, Birgit Pröll, Werner Retschitzegger, Wieland Schwinger, Johannes Schönböck, Manuel Wimmer, Stephan Lechner.
User profile integration made easy: model-driven extraction and transformation of social network schemas. In WWW (Companion Volume) 2012: 939-948. ACM 2012.
[ pdf | bib | abstract | doi ]

Angelika Kusel, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, Ralph Mayr, Johannes Schönböck.
Ontology-Driven Generation of Multi-View Modeling Tools. In Software Engineering 2012: IASTED 2012.
[ bib | abstract | doi ]

Norbert Baumgartner, Stefan Mitsch, Andreas Müller, Werner Retschitzegger, Andrea Salfinger, Wieland Schwinger.
The Situation Radar – Visualizing Collaborative Situation Awareness in Traffic Control Systems, In ITS World Congress 2012.
[ abstract ]

Wolfgang Gottesheim, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, Norbert Baumgartner.
SemGen - Towards a Semantic Data Generator for Benchmarking Duplicate Detectors. In DASFAA Workshops 2011: 490-501. Springer 2011.
[ pdf | bib | abstract | doi ]

Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger
Towards Modeling Dynamic Behavior with Integrated Qualitative Spatial Relations. In ER Workshops 2011: 271-280. Springer 2011.
[ pdf | bib | abstract | doi ]

Norbert Baumgartner, Wolfgang Gottesheim, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger.
Reasoning on Data Streams for Situation Awareness. In KEOD 2011: 407-412. SciTePress 2011.
[ bib | abstract ]

Stefan Mitsch, Wolfgang Gottesheim, Franz Hermann Pommer, Birgit Pröll, Werner Retschitzegger, Wieland Schwinger, Robert Hutter, Gustavo Rossi, Norbert Baumgartner.
Making workflows situation aware: an ontology-driven framework for dynamic spatial systems. In iiWAS 2011: 182-188. ACM 2011.
[ pdf | bib | abstract | doi ]

Elisabeth Kapsammer, Stephan Lechner, Stefan Mitsch, Birgit Pröll, Werner Retschitzegger, Wieland Schwinger, Manuel Wimmer, Martin Wischenbart.
Towards a Reference Model for Social User Profiles: Concept & Implementation. In PersDB 2011: 6. VLDB 2011.
[ pdf | bib | abstract ]

Norbert Baumgartner, Wolfgang Gottesheim, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger.
Situation Prediction Nets - Playing the Token Game for Ontology-Driven Situation Awareness. In ER 2010: 202-218. Springer 2010.
[ pdf | bib | abstract | doi ]

Wolfgang Gottesheim, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, Norbert Baumgartner.
WorkAware - Situation-aware Workflow Management. In KMIS 2010: 246-252. SciTePress 2010.
[ bib | abstract ]

Norbert Baumgartner, Wolfgang Gottesheim, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger.
Towards Duplicate Detection for Situation Awareness Based on Spatio-temporal Relations. In ODBASE 2010: 1097-1107. Springer 2010.
[ pdf | bib | abstract | doi ]

Norbert Baumgartner, Wolfgang Gottesheim, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger.
Improving Situation Awareness in Traffic Management. In QDB 2010: 5. ACM 2010.
[ pdf | eprint | bib | abstract ]

Werner Kurschl, Stefan Mitsch, Johannes Schönböck.
Modeling Distributed Signal Processing Applications. In BSN 2009: 103-108. IEEE Computer Society 2009.
[ pdf | bib | abstract | doi ]

Werner Kurschl, Stefan Mitsch, Johannes Schönböck.
Modeling Situation-Aware Ambient Assisted Living Systems for Eldercare. In ITNG 2009: 1214-1219. IEEE Computer Society 2009.
[ pdf | bib | abstract | doi ]

Norbert Baumgartner, Wolfgang Gottesheim, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger.
On Optimization of Predictions in Ontology-Driven Situation Awareness. In KSEM 2009: 297-309. Springer 2009.
[ pdf | bib | abstract | doi ]

Norbert Baumgartner, Wolfgang Gottesheim, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger.
"Same, Same but Different" A Survey on Duplicate Detection Methods for Situation Awareness. In ODBASE 2009: 1050-1068. Springer 2009.
[ pdf | bib | abstract | doi ]

Werner Kurschl, Stefan Mitsch, Johannes Schönböck.
An Engineering Toolbox to Build Situation Aware Ambient Assisted Living Systems. In BroadCom 2008: 110-116. IEEE Computer Society 2008.
[ pdf | bib | abstract | doi ]

Werner Kurschl, Wolfgang Gottesheim, Stefan Mitsch, Rene Prokop, Johannes Schönböck.
Automatic Position Determination of Fixed Infrastructure Sensor Network Nodes based on Topology Sensing and Maps. In ICWN 2008: 17-22. CSREA Press 2008.
[ bib | abstract ]

Werner Kurschl, Stefan Mitsch, Johannes Schönböck, Wolfgang Beer:
Modeling wireless sensor networks based context-aware emergency coordination systems. In iiWAS 2008: 117-122. ACM 2008.
[ pdf | bib | abstract | doi ]

Werner Kurschl, Wolfgang Gottesheim, Stefan Mitsch, Rene Prokop, Johannes Schönböck, Wolfgang Beer.
A Two-Layered Deployment Scheme for Wireless Sensor Network based Location Tracking. In ITNG 2008: 726-730. IEEE Computer Society 2008.
[ pdf | bib | abstract | doi ]

Werner Kurschl, Stefan Mitsch, Rene Prokop, Johannes Schönböck.
Gulliver-A Framework for Building Smart Speech-Based Applications. In HICSS 2007: 30. IEEE Computer Society 2007.
[ pdf | bib | abstract | doi ]

Werner Kurschl, Wolfgang Gottesheim, Stefan Mitsch, Rene Prokop, Johannes Schönböck.
Evaluation of a Mobile Multimodal Application Design - Major Usability Criteria and Usability Test Results. In ICMB 2007: 68. IEEE Computer Society 2007.
[ pdf | bib | abstract ]

Werner Kurschl, Stefan Mitsch, Rene Prokop, Johannes Schönböck.
Development issues for speech-enabled mobile applications. Software Engineering 2007: 157-168. GI 2007.
[ pdf | bib | abstract | doi ]

Werner Kurschl, Stefan Mitsch, Rene Prokop.
SmartDOTS - A Framework for Efficient Data Synchronization on Mobile Devices. In ITNG 2006: 300-305. IEEE Computer Society 2006.
[ pdf | bib | abstract | doi ]

Werner Kurschl, Stefan Mitsch, Rene Prokop.
SelectiveDES: A Distributed Event Service Add-On for Invocation-Based Middleware supporting Selective Multi-Channel Communication and Notification Delivery. In ITNG 2006: 328-333. IEEE Computer Society 2006.
[ pdf | bib | abstract | doi ]

Werner Kurschl, Stefan Mitsch, Rene Prokop.
Mobile Work Clearance Management - Challenges and Solutions. In MMS 2006: 9-20. GI 2006.
[ bib | abstract | doi ]