Wednesday, February 8, 2017 - 9:00am to 11:00am
Location:7101 Gates Hillman Center
Speaker:FLORIAN ADOLF and SEBASTIAN SCHIRMER, German Aeropsace Center - DLR http://www.dlr.de/ft/en/desktopdefault.aspx/tabid-1336/1837_read-32330/
As capabilities, technology readiness and autonomy of unmanned aircraft matures, increasingly important aspects that come into consideration are these of correctness, failsafe-ness, robustness and health management. Furthermore, debugging and analysis of complex systems is an important part of development activities. Runtime monitoring of relevant properties and system requirements is a key technique to support such concepts. A suitable monitoring approach for a cyber-physical system has to be efficient and capable of supervising various specifications, possibly relating different data sources and data history. In this paper we present a formal approach for log-analysis and monitoring for the DLR ARTIS framework using a tool for the stream-based specification language LOLA, currently developed at Saarland University, for the runtime monitoring of formal specifications. The formal language is based on the concepts of linear temporal logic but is actually more expressive, for example it is possible to calculate probabilities instead of Boolean values. The formal methodology of runtime monitoring is introduced in the context of system health management, and application scenarios are detailed. The monitoring tool and its formal specification language LOLA is briefly described and the integration into the DLR ARTIS framework, phase one offline monitoring, and phase two online monitoring, is shown. Finally, examples show the benefits of using LOLA within the framework.—Florian-Michael Adolf has worked almost 15 years as a roboticist and got actively involved with many different challenges in perception, learning, planning and control. For example, he started working with camera-based object detection and autonomous transportation before he was working on real-time bision based soccer playing behaviors for a team of autonomous soccer robots (aka RoboCup). After he received my M.Sc. in Autonomous Systems in 2006, he specialized my research work in real-time sampling-based motion planning for unmanned rotocraft. Florian leads team of highly motivated researchers since 2013, who improve his initial work towards other unmanned aircraft types as well as the complex task of validation and verification thereof. Florian's daily work comprises not only technical and research work, but also international meetings with related special interest groups. But in order to keep his "feet on the ground", he tries to balance between theoretical and practical work as! well as related committee efforts. Through his work, he contributes to a better understanding as well as a feasibility analysis of approaches from various disciplines; i.e. an overall system perspective rather than a sole disciplinary one.Sebastian Schirmer received his M.Sc. in Computer Science from Saarland University in 2016. During his studies as a research assistant he implemented the formal language LOLA that is used for monitoring approaches across different applications. With his thesis he achieved to augment athe unmanned rotorcraft guidance and control software framework with formal methods using LOLA. In particular, he applied monitoring to support the offline log-file analysis as well as online capabilities in order to enrich the information of the overall system states. This way he was able to analyze the system for assurance purposes "in-time". In 2017, he joined the German Aerospace Center (DLR) to continue working on Formal Methods and other Model-based assurance methods for unmanned aircraft.