Reactive Control Meets Runtime Verification: A Case Study of Navigation
19th International Conference on Runtime Verification, RV 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019, Porto, Portekiz, 8 - 11 Ekim 2019, cilt.11757 LNCS, ss.368-374, (Tam Metin Bildiri)
- Yayın Türü: Bildiri / Tam Metin Bildiri
- Cilt numarası: 11757 LNCS
- Doi Numarası: 10.1007/978-3-030-32079-9_21
- Basıldığı Şehir: Porto
- Basıldığı Ülke: Portekiz
- Sayfa Sayıları: ss.368-374
- Açık Arşiv Koleksiyonu: AVESİS Açık Erişim Koleksiyonu
- Boğaziçi Üniversitesi Adresli: Hayır
Özet
This paper presents an application of specification based runtime verification techniques to control mobile robots in a reactive manner. In our case study, we develop a layered control architecture where runtime monitors constructed from formal specifications are embedded into the navigation stack. We use temporal logic and regular expressions to describe safety requirements and mission specifications, respectively. An immediate benefit of our approach is that it leverages simple requirements and objectives of traditional control applications to more complex specifications in a non-intrusive and compositional way. Finally, we demonstrate a simulation of robots controlled by the proposed architecture and we discuss further extensions of our approach.