My funding supports research in a number of topics listed under Current Research Topics. Further details can be found in my CV.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

Current Funding

Completed Projects


Monitoring, Testing, Verification and Validation of Cyber-Physical Systems

Temporal logics have been proven to be an extremely useful formalism for the property based verification or testing of software and hardware systems. Several critical bugs in protocols and designs have been detected using software toolboxes that have resulted from this line of research. Even though there is a dire need for the property based validation and verification of mixed-signal and, in general, Cyber-Physical Systems (CPS), similar breakthrough technologies have not yet been developed. The consequences of not having that capability can often lead to catastrophic failures. For example, cruise control systems that do not disengage under certain operating conditions or infusion pumps that may overdose patients. Embedded computers (both hardware and software) in such safety critical systems need to be verified to ensure that such behaviors will not occur.

We are developing breakthrough technologies for testing and verification of CPS. Our main research direction develops the necessary theories and tools in order to enable what we call Robustness Guided Model Checking (RGMC).

Central to the objectives of this research is the robust interpretation of Metric Temporal Logic (MTL) (and, hence, Linear Temporal Logic (LTL)) specifications over signals that take values in metric spaces. For such signals, which are generated by systems whose states are equipped with nontrivial metrics, for example continuous or hybrid, robustness is not only natural, but also a critical measure of system performance. Thus, we utilize multi-valued semantics for MTL formulas, which capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance ε from unsatisfiability. Any other signal that remains ε-close to the initial one also satisfies the same MTL specification under the usual Boolean semantics. The robust semantics have found several applications on diverse problems such as (i) robust and/or statistical testing of CPS, (ii) computation of satisfiability and estimation of robustness for real-time formulas with continuous time semantics using discrete time reasoning on the sampled signal and (iii) monitoring of MTL properties of CPS for assurance.

RGMC utilizes the theory of robustness for real-time temporal logics and the theory of approximate bisimulations to infer the behavior of a neighborhood of system trajectories from a single system trajectory. A major advantage of this work is that the more robust the system is with respect to the specification the easier it is to verify its properties. Our [software tools] have been applied to many applications from the automotive and the medical device industries ([references]). Finally, our tools can be utilized at various stages of the Model Based Development (MBD) process.

S-Taliro support in the Model-Based Development (MBD) of Cyber-Physical Systems (CPS). (1) Iterative development and testing/verification of model; (2) Hardware/Processor-In-the-Loop conformance testing; (3) Tuning and testing/verification of prototype system; (4) Monitoring of deployed system.

Human-Robot Interaction and Planning

Consider a mobile robot that has to navigate through a labyrinth-like environment in order to perform a complex task. Such tasks (specifications) could be stated in natural or structured language by the user of the robot. For example, "Visit rooms A, B and C while avoiding room D" and "Patrol rooms A, B and C. If you detect a fire, call the fireman." could be two such input specifications. Nowadays, such scenarios are increasingly becoming a reality through new robots that hit the market. For example, [RP-VITA Telemedicine Robot] is a semi-autonomous remote presence robot that can navigate inside hospital corridors.

The interesting aspect of these types of specifications is that they can be captured by [temporal logic formulas]. However, writing and reading such specifications in temporal logics is a task that requires mathematical training. Therefore, the methods developed for robot motion and action planning through temporal logics become unapproachable to persons without the appropriate mathematical background. At the same time, automatic language comprehension by computing systems is not at a stage where it can be readily deployed for human robot interaction - especially - in safety critical scenarios.

This research investigates various methods for providing human user input to autonomous robots. One direction of this research focuses on visual specification languages for intuitive robot programming by non-expert roboticists. Another research direction is utilizing structured English in order to avoid issues that arise in analyzing ambiguous sentences in natural language.

[See fun Capstone projects and our tool LTLvis]

In order to develop a truly user friendly temporal logic planning system, we need to provide feedback to the user when the planning stage fails. That is, when the temporal logic specification cannot be realized or satisfied in the current environment under the current system dynamics, then the high-level synthesis framework cannot simply report a failure. We need a feedback system to recommend to the user specifications that are realizable on our particular system and environment. This is extremely important since the human user might not be aware of the current environment or the capabilities of the robotic system. Of course, such recommendations cannot be arbitrary formulas which happens to be satisfiable on our particular model (i.e., environment and system). For example, it is easy to see that the specification "always true" (i.e., "do not do anything") is a valid formula which is true on every possible model. Hence, these new specification recommendations must be as close as possible to the original intentions of the user.

Hybrid System Synthesis from High-Level Specifications

Complex operating regions as well as involved control specifications necessitate the development of hybrid control laws for the regulation of a dynamical system. A very characteristic example of such a system is a mobile robot that has to navigate through a labyrinth-like environment in order to perform a complex task. Such tasks (specifications) can be stated using Temporal Logics. For example, "(!D U A) /\ (!D U B) /\ (!D U C)" could be a formula for the specification "Visit rooms A, B and C while avoiding room D". The design by hand of non-trivial hybrid systems that have to satisfy complicated specifications is a tedious and error-prone procedure. Moreover, the verification of such systems in most of the cases is an undecidable problem. This project investigates certain classes of systems for which the synthesis problem from temporal logic specifications can be efficiently solved in a bottom-up or top-down fashion. In a bottom-up approach the controllers are provided and the synthesis procedure attempts to compose the controllers in such a way that the trajectories of the final system satisfy the specification. A top-down approach has the advantage over a bottom-up approach that the method does not have to look for a solution over a restricted set of controllers. The method to design the controllers depends on the respective controller specifications.


Techniques for Embedded System and Software Assurance (NEC Labs America)

For this project, a framework for the robustness analysis of Simulink simulations was developed. The main theoretical machinery that was employed for the analysis was self-validated arithmetics (interval and affine arithmetic). The goal of the project was to study the robustness and correctness of Simulink simulations under system uncertainties, numerical errors and floating point rounding errors. The outcome of the project was the Matlab toolbox RobSim which can analyze continuous-time, discrete-time and mixed-signal systems.

Modeling and Design of UAVs (University of Pennsylvania)

This project concerned the development of a number of autonomous Unmanned Aerial Vehicles (UAV) at the University of Pennsylvania. The following tasks were completed: (i) design of components for the UAVs, (ii) aerodynamic and stractural modeling of the UAVs, and (iii) hybrid system modeling of the UAVs when controlled by the autopilot.

Extended Ant Colony Optimization (National Technical University of Athens)

Ant Colony Optimization (ACO) is an innovative optimization method inspired by ants' behavior during foraging. ACO was introduced by M. Dorigo and applied to discrete optimization problems. In this work, the Extended Ant Colony Optimization (EACO) method was introduced for dealing with continuous optimization problems. EACO has been successfully applied to the problem of Inverse Design of Aerodynamic Shapes (IDS).


S-TaLiRo Tool Suite [Get tools]

A suit of tools for the analysis of continuous and hybrid dynamical systems using linear time temporal logics. S-TaLiRo (Systems TaLiRo) is a software toolbox for Matlab for the temporal logic falsification of Hybrid Automata and Matlab/Simulink models. S-TaLiRo is based on the principle of the Robustness Guided Model Checking (RGMC). TaLiRo is a software toolbox for Matlab for the temporal logic robustness analysis of discrete time signals that take values in metric spaces.

S-TaLiRo has been applied to numerous challenging applications from the automotive and medical device industries. [Visit the S-TaLiRo website] for more details.

In 2012, S-Taliro was nominated as a technological breakthrough by the industry! [Read the report]

LTLvis: A Graphical Language for LTL Motion and Mission Planning [SVN/Git]

Linear Temporal Logic (LTL) is gaining increasing popularity as a high level specification language for robot motion planning due to its expressive power and scalability of LTL control synthesis algorithms. This formalism, however, requires expert knowledge and makes it inaccessible to non-expert users. LTLvis is a graphical specification environment to create high level motion plans to control robots by converting a visual representation of the motion/task plan into an LTL specification. The visual interface is built on the Android tablet platform and provides functionality to create task plans through a set of well defined gestures and on screen controls. It uses the notion of waypoints to quickly and efficiently describe the motion plan and enables a variety of complex LTL specifications to be described succinctly and intuitively by the user without the need for expert knowledge and understanding of LTL. Thus, it opens avenues for its use by personnel in military, warehouse management, and search and rescue missions.

[Try the app!]. Read this [MS thesis] for instructions.

Model-Based Development for Multi-iRobot Toolbox (MBDMIRT) [v1.1, SVN]

MBDMIRT is a Simulink-based toolbox designed to provide the means to acquire and practice Model-Based Development (MBD) skills necessary to design real-time embedded systems. The MBDMIRT toolbox runs under MATLAB/Simulink to simulate the movements of multiple iRobots and to control, after verification by simulation, multiple physical iRobots.

The MBDMIRT toolbox reuses and augments the open-source MATLAB-Based [Simulator for the iRobot Create] from Cornell University to run the simulation. For physical control, the MBDMIRT utilizes the [MATLAB Toolbox for the iRobot Create (MTIC)] from United States Naval Academy to command the physical iRobots.

The MBDMIRT toolbox supports timers in both simulation and physical control. In addition to the build-in sensors of an iRobot, the toolbox can simulate user-added sensors such as an Overhead Localization System (OLS), sonar sensors, a camera, and a LIDAR. For physical iRobot control, the MBDMIRT supports the StarGazer OLS manufactured by HAGISONIC, Inc.

See [videos] of the toolbox in action. Get a ZIP for [MBDMIRT Version 1.1] or access the [SVN repository] for the latest version.

NAO MBD Simulink/Stateflow Toolbox (NAOMBD) [SVN]

As the complexity of robotic systems and applications grows rapidly, development of high-performance, easy to use, and fully integrated development environments for those systems is inevitable. Model-Based Design (MBD) of robotic systems using software such as Simulink from MathWorks is gaining in popularity. Such systems provide tools for modeling, simulation, verification and in some cases automatic code generation for desktop applications, embedded systems and robots.

For real-world implementation of models on the actual robot hardware, those models should be converted into compilable machine code either manually or automatically. Due to the complexity of robotic systems, manual code translation from model to code is not a feasible optimal solution so we need to move towards automated code generation for such systems. MathWorks offers code generation through the Coder products. However in order to fully exploit the power of model-based design and code generation tools for robotic applications, we need to enhance those software systems by adding and modifying toolboxes, files and other artifacts as well as developing guidelines and procedures. In this toolbox, an effort has been made to propose a guideline as well as a Simulink library, StateFlow interface API and C/C++ interface API to complete this toolchain for NAO humanoid robots. Thus, the model of the hierarchical control architecture can be easily and properly converted to code and built for implementation.

The toolbox is available to [download] which includes the StateFlow Interface API, Simulink Library (for simulation and code generation) and C/C++ Interface API. You can also read [Ramtin's thesis].

Software Tools


Systems' TemporAl LogIc RObustness


Temporal Logic Minimal Specification Revision and Planning Toolbox


Cooperative Pathfinding in Distributed Systems with Limited Sensing and Communication Range


A Graphical Language for LTL Motion and Mission Planning


Model-Based Development for Multi-iRobot Toolbox


NAO Model-Based Development Simulink/Stateflow Toolbox

CPSLab Robots


Home :: Research :: Publications :: Miscellaneous
Admin: G. Fainekos // Design: O. Fainekos // Copyright @ Georgios Fainekos // Last update@2014.01.20