Using Formal Modeling With an Automated Analysis Tool to Design and Parametrically Analyze a Multirobot Coordination Protocol: A Case Study
- 16 April 2007
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans
- Vol. 37 (3), 285-297
- https://doi.org/10.1109/tsmca.2006.886378
Abstract
Many robot systems employ logic-based or reactive controllers, making them hybrid systems (i.e., mixed discrete continuous). However, designing such control laws in a systematic manner remains a challenging task. In this paper, we apply the formal modeling paradigm to a team of mobile robots. The linear hybrid automata modeling framework is used to describe the high-level design, and the verification software HyTech is used for symbolic analysis of the description. The goal is to symbolically quantify system-level performance as a function of the design parameters, for the purpose of optimizing and synthesizing design parameters, verifying safe operation, and quantitatively exploring tradeoff issues. In order to make the analysis tractable, a series of restrictive assumptions and simplifications must be made-some dictated by the linear hybrid automata model and others necessitated by computational cost. We comment on the restrictiveness of these assumptions and the overall utility of this automated analysis approach in designing complex robotic systemsKeywords
This publication has 18 references indexed in Scilit:
- Hierarchical modeling and analysis of embedded systemsProceedings of the IEEE, 2003
- A formalism for the composition of concurrent robot behaviorsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A Framework and Architecture for Multi-Robot CoordinationThe International Journal of Robotics Research, 2002
- The d/dt Tool for Verification of Hybrid SystemsLecture Notes in Computer Science, 2002
- Verification of infinite-state dynamic systems using approximate quotient transition systemsIEEE Transactions on Automatic Control, 2001
- Sequential Composition of Dynamically Dexterous Robot BehaviorsThe International Journal of Robotics Research, 1999
- HYTECH: a model checker for hybrid systemsInternational Journal on Software Tools for Technology Transfer, 1997
- Computer-aided verificationIEEE Spectrum, 1996
- Automatic symbolic verification of embedded systemsIEEE Transactions on Software Engineering, 1996
- The algorithmic analysis of hybrid systemsTheoretical Computer Science, 1995