My current research focuses on knowledge representation and reasoning for self-adaptive systems,
autonomy requirements engineering, development and verification of autonomous systems, safety properties
and compilers. More broadly, my research interests are in software development methodologies for autonomous
and self-adaptive systems along with capturing autonomy requirements and modeling safety properties.
Another very important trend of my research focuses on compiler design and implementation with LLVM. A part
from the main research, my research interests include: machine learning, distributed computing, formal methods,
software engineering, programming languages, cyber forensics, sensor networks, real-time systems,
embedded systems, home automation, network protocols and multiagent systems.
Significant Research Projects
Extended ARE Framework
(Lero 3 Hub B1 Project #1)
In this project, I'm further developing the theory behind the ARE Framework (see the project description below)
along with full implementation of supporting tools that shall allow software engineers tackle autonomy
requirements in terms of efficient and comprehensive means for their elicitation, documentation, formalization,
implementation, and validation. The R&D in this project address some of the following fundamental challenges of
autonomous and adaptive systems:
- engineering autonomy requirements
- modelling self-adaptation
- artificial awareness
Note that both ASSL (Autonomic System Specification Language) and KnowLang (frameworks developed by myself -
see the projects below) shall be adapted and integrated with ARE as formal notations to specify autonomy
requirements in regard to both event-driven and goal-oriented autonomy.
Adaptive Systems Test Bed and Robotics Platform
(Lero 3 Hub B1 Project #2)
This project is about the R&D of a special Test Bed for Adaptive Systems (TBAS) where such
systems can be tested under simulated conditions in both virtual and physical testing environments.
With such a TBAS we shall be able to efficiently test adaptive behavior by validating self-* objectives
through evaluation of the system’s ability to perceive both the internal and external environments and
react to changes. With TBAS, we target the evaluation of features that manifest the system's awareness
about situations and conditions, and the system's ability to self-adapt to those situations and conditions
when adaptation is required. The foundation of TBAS is the ARE Framework. In this project, I am developing two test platforms:
- A fully virtual simulation environment (virtual TBAS) where thousands of virtual adaptive entities (VAEs)
can be tested both individually or/and as an "intelligent swarm" where VAEs interact not only with the
environment, but also internally.
- A test platform based on WiFi-communicating, mini-computerized and robotized platforms, yet capable
of running a fully-functional VAE. Such a robotized platform (Lero Robotics Platform - LRP) is going
to be autonomously controlled by the hosted VAE, and shall be equipped with a variety of plug-in sensors
such as: light detectors, microphones, smoke detectors, motion detectors, humidity detectors, high-speed
thermometer, barometer, etc.
The R&D in this project address the following fundamental challenges of autonomous and adaptive systems:
- Simulation and testing of adaptive systems; behavior testing by validating self-* objectives;
reasoning about autonomy properties.
- Verification and validation of adaptive systems: automatic detection of unintended interactions
- Adaptation and human-computer interaction: evaluation of partial autonomy.
Verification of Adaptive Systems
(Lero 3 Hub B1 Project #3)
This project deals with the R&D of an Adaptive Behavior Verification (ABV) approach, providing both a tool
chain and methodology for verifying self-adaptive systems. The ABV approach shall consist of the following parts:
- a stability analysis capability that identifies instabilities given a system model and partitions the
system model into stable and unstable component models;
- a state-space reduction capability that prunes the state space of an unstable component model
without loss of critical fidelity;
- high performance computing (HPC) simulations to explore component behavior over a wide range of
an unstable component’s reduced state space and produce a statistical verification for the component;
- a compositional verification capability that integrates individual component verifications;
- operational monitors to detect and take action to correct undesired unstable behavior of the system
LLVM Compiler for In-Flight SW Development and Validation Process: LLVM Backend for LEON Processors
(a contractual project with ESA)
The LLVM LEON backend resulted from a joint project between Lero - the Irish Software Center,
Cobham Gaisler as a subcontractor providing the test suite, and the ESTEC division of ESA. The project
targeted the development of a compiler that adapts and extends the LLVM toolchain to the LEON family of
processors which are widely used in various ESA computerized systems, such as spacecraft. Only two people
were involved from Lero to work in this project: I was the project leader, software engineer and developer,
and a system programmer was hired to implement errata fixes and to perform testing.
The LLVM LEON backend project run as a software engineering endeavor with the emphasis put on compiler
correctness. All the traditional software process stages were performed in a rather spiral manner where
multiple iterations led to the final product. During these iterations, various artifacts were produced,
including documentation, backend implementation, and a test suite for integration testing. In addition,
in the curse of this project, a unit test plan was defined and proper unit tests were developed to test
the correctness of particular features of the SPARC/LEON backend. The unit-testing goal was to demonstrate
that each instruction is correctly generated and encoded. My presentation at ESA's final presentation days
can be seen here:
Autonomous Software Systems Development Approaches
(Methods and Tools for On-Board Software Engineering (Task 2), a contractual project with ESA)
ESA is currently targeting the R&D of autonomous spacecraft and autonomous control systems (e.g., ExoMars).
Such autonomous systems will enable spacecraft to adapt to unforeseen situations making them more resilient and
able to self-adapt, self-repair and become more fit-for-purpose.
In this joint project with ESA, I have solely developed the Autonomy Requirements Engineering Approach (ARE)
to help developing these types of systems. ARE converts adaptation issues into autonomy requirements where a
technique known as Goal-Oriented Requirements Engineering (GORE) is used along with a model for Generic Autonomy
Requirements (GAR). ARE was applied to a proof-of- concept case study, to capture autonomy requirements of the
ESA’s BepiColombo Mission to Mercury (see my presentation at ESA's final presentation days here:
Note that this research in autonomous systems will not only benefit future space missions but also exploration
robots, drones and autonomous cars. My work in this project inspired the book
"Autonomy Requirements Engineering for Space Missions".
Note that ARE relies on another work of mine - the KnowLang
formal language, to formally specify the elicited autonomy requirements.
KnowLang - a Formal Language for Knowledge Representation in Autonomic Service-Component Ensembles
(a work package of the ASCENS FP7 Project)
One of the significant scientific contributions that we achieved with the
ASCENS Project is related to
knowledge representation and reasoning (KR&R) for self-adaptive systems. Note that self-adaptive systems must
be aware of their physical environment and whereabouts, as well as of their current internal status. This
ability helps software intensive systems sense, draw inferences, and react by exhibiting self-adaptation.
A common understanding about the process of self-adaptation is the ability of a system to autonomously monitor
its behaviour and eventually modify the same according to changes in the operational environment, or in the
system itself. The paradigm requires that the system engages in various interactions where important structural
and dynamic aspects of the environment are perceived. Therefore, it is of major importance for a self-adaptive
system to acquire and structure comprehensive knowledge in such a way that it can be effectively and efficiently
processed, so such a system becomes aware of itself and its environment.
ASCENS was a multi-institutional, yet multinational, four-year long project where as part of the Lero's mandate
in this project, I solely performed the R&D of KnowLang,
a special framework for KR&R. KnowLang provides a
special knowledge context and a special reasoner operating in that context. The approach is formal and
demonstrates how knowledge representation and reasoning help to establish the vital connection between knowledge,
perception, and actions realizing the self-adaptive behavior. The knowledge is used against the perception of
the world to generate appropriate actions in compliance to some goals and beliefs.
Knowledge specified with KnowLang takes the form of a Knowledge Base (KB) that outlines a Knowledge
Representation (KR) context. The KnowLang Reasoner operates in this context to allow for knowledge querying and
update. In addition, the reasoner can infer special self-adaptive behavior. A key feature of KnowLang is a
formal language (KnowLang notations) with a multi-tier knowledge specification model allowing for integration
of ontologies together with rules and Bayesian networks. The language aims at efficient and comprehensive
knowledge structuring and awareness based on logical and statistical reasoning where additive probabilities
are used to represent degrees of belief. Other remarkable features are related to knowledge cleaning
(allowing for efficient reasoning) and knowledge representation for elf-adaptive behavior.
The KnowLang Reasoner was used to perform simulation of awareness for ASCENS ensembles. A variety of
knowledge bases were implemented in KnowLang notation, e.g., eMobility (a case study provided by Volkswagen),
scientific clouds, swarm robotics, etc. Moreover, KnowLang was completed as the formal specification language
of ARE, the Autonomy Requirements Engineering approach, and has been used to formalize the autonomy
requirements of the ESA's BepiColombo mission (the specification model is described in various publications,
including the ARE book
"Autonomy Requirements Engineering for Space Missions").
Moreover, KnowLang has inspired over 50 publications and has been presented at various seminars, conferences,
and scientific schools (e.g., the spring school for Ph.D. students on Engineering Collective Autonomic Systems
(ECAS), in Lucca, Italy, March 23-27, 2017).
Verification of Adaptive Systems
(a prospective joint project with Lockheed Martin and NASA)
Adaptive systems are being proposed for combat, security and other critical missions. Adaptive systems
are systems that autonomously adjust their behavior due to unanticipated events, changes in environment, etc.
Such systems may exhibit unstable behavior and must be verified before they are used in mission critical
situations. However, current verification methods do not scale to support the astronomical state space of
adaptive systems. This research focuses on a new approach to verification of adaptive systems that relies on
existing and enhanced stability analysis techniques together with high performance simulation, state space
reduction and compositional verification.
Patch Generation and Self-healing
(a work package of the FastFix FP7 project)
This research is in the area of autonomic systems and targets a software platform helping developers
identify symptoms of execution errors, performance degradation, or changes in user behavior. By using correlation
techniques, the platform shall also support failure replication in order to identify incorrect execution patterns
and, in particular cases, automatically generate and deploy remedial patches. Thus, after the problem root cause
is identified, a way is needed to generate patches to fix that defect, and if possible, do it automatically. Once
the patch is ready, a way to deploy it in the application platform must be addressed.
Developing Autonomic Systems
The rapidly growing field of autonomic computing (AC) promises a new approach to developing complex
computing systems. Concluding that AC is a viable long-term solution, many major software vendors—such as
IBM, HP, Sun, and Microsoft—are researching programs to create computer systems that manage themselves.
However, their research efforts focus mainly on making individual components of particular systems more
self-managing, rather than solving the problem of autonomic system (AS) development. Thus, 10 years after
the initial AC announcement, we still have far to go before establishing an autonomic culture. This goal eludes
us because traditional development barely addresses some AC features. Further, the field of AC does not
currently provide researchers with a clear idea of what AS development requires. Thus, whereas the AC
principles and goals are clear, we still need techniques and technologies that provide programming concepts
for implementing ASs. This research focuses on methodologies for developing ASs. The grand challenges to
overcome in this research are: self-* requirements, knowledge, awareness, monitoring, adaptability, autonomy,
dynamicity, robustness, mobility, etc. In the curse of this research, we have been working on formal approaches
to AC. Formal methods could facilitate AS development, while AC formalisms can help developers craft a
well-defined formal semantics that makes the AC specifications a base from which developers can design,
implement, and verify autonomic systems.
Part of this research focuses on
ASSL (Autonomic System Specification Language),
a framework dedicated to
autonomic computing (AC) that addresses the problem of formal specification and code generation of autonomic
systems. ASSL implies a multi-tier structure for specifying autonomic systems and targets the generation of
an operational framework instance from an ASSL specification. This framework is conceived to help the AC
researchers with problem formation, system design, system analysis and evaluation, and system implementation.
Both model checking and visual modeling with ASSL form my current research trend on ASSL. The objectives
of model checking with ASSL are focused on developing a model-checking mechanism that allows for handling
logical errors. Here, the threefold objective is:
- Develop a model-checking mechanism for ASSL that takes as input an ASSL specification and produces as
output a finite state-transition system such that a specific property in question is satisfied if and only
if the original ASSL specification satisfies that property.
- Develop a mechanism for ASSL embedding the Java PathFinder tool (developed at NASA Ames) to perform
post-implementation model checking on ASSL-generated autonomic systems.
- Develop a mechanism for ASSL allowing for mapping ASSL specifications to special Service Logic Graphs
supporting reverse model checking and games.
The goal of visual modelling with ASSL is to develop UML-like presentation of the ASSL tiers where a visual
environment that implements the ASSL mathematical models will help expert designers to efficiently build
autonomic systems via modeling customizable ASSL specifications with the drag-and-drop technique.
Developing and prototyping intelligent swarm systems and sensor networks with ASSL is another research trend I
am currently pursuing. Currently, the ASSL framework provides a toolset allowing ASSL specifications to be
edited, syntactically and semantically validated, and Java code to be generated. These features of ASSL
helped the latter be used successfully to specify autonomic features and generate prototype models for a
few systems including two NASA projects - the Autonomous Nano-Technology Swarm Concept Mission and the
Voyager Mission. In both cases, the generated prototype models helped to simulate space exploration
missions and validate features through experimental results. Here, the benefits come from the ability
to simulate exploration missions with hypothesized autonomic features.