Timed-Altarica-To-Fiacre-Translator/doc/Rapport post-doc/5-conclusions.tex

%%%\section{Conclusion and Related Work}
\label{sec:Conclusion}

Our work is concerned with the modelling and analysis of safety properties 
in the presence of time constraints. 


We concentrate on a
particular safety property, called \emph{loss detection convergence},
for failures
propagation, meaning that the system applies an appropriate and timely response
(e.g. isolation) to the occurrence of a fault before the failure is
propagated and produces unwanted system behaviours. Similar problems
were addressed in~\cite{thomas2013}, where the authors describe a
process to model FDIR architecture (for use on-board satellites) that
requires to take into account failure propagation time, failure
detection time, and failure recovery time. However, these needs are not matched by 
an effective way to check for safety. Our approach provides a solution to
model these timing constraints within AltaRica. We also provide an
automatic transformation from Time AltaRica models into one of the
input formats of Tina. We show that two interesting
problems---computing ``timed cuts'' and bounding the convergence
latency of a node---can be reduced to a decidable model-checking
problem.

Several works have combined model-checking and AltaRica, the
archetypal example being the MEC tool~\cite{griffault2004mec} that was
developed at the same time than the language. More recently, Bozzano
et al~\cite{bozzano2012} have defined a transformation from AltaRica
Dataflow to the symbolic model-checker NuSMV. While this tool does not
support complex timing constraints, it offers some support for Dirac
laws (and implicit priorities) by encoding an ad-hoc scheduler. The
use of symbolic model-checking techniques is interesting in the case
of models with a strong combinatorial blow up, like for instance model
HYDRO of Sect.~\ref{sec:sect4}. Nonetheless, even though Tina also
includes BDD-based tools, no approaches allow to combine the advantages
of both realtime and symbolic model-checking techniques.

Realtime techniques are central to our approach. We define an
extension of AltaRica where timing constraints can be declared using
{temporal laws} of the form \code{law (evt) = "[a,b]"}, with a
semantics inspired by Time Petri nets. As a result, we can apply on
AltaRica several state space abstractions techniques that have been
developped for ``timed models'', such as the use of DBM and state
classes~\cite{berthomieu2004tool}. In a different way, Cassez et
al.~\cite{pagetti2004} have proposed an extension of AltaRica with
explicit ``clock variables'', inspired by Timed Automata, where clocks
are real-valued flow variables that can be used inside the guards of
events.
%%
% (Which means that there are restrictions on the type of equations
% one can use in the \code{assert} declaration of a node.)
%%
% They also define an algorithm to compile this extension into
% Uppaal~\cite{larsen1997uppaal}. 
Their work is mainly focused on the verification of behavioural
properties and centers on the encoding of urgency and priorities
between events, two notions that are naturally offered in
Fiacre. Also, our extension is less invasive. If we ignore the
\code{extern} declaration then we obtain valid AltaRica code. More
research is still needed to further the comparison between these two
approaches in the context of safety assessments.

Aside from these works on AltaRica, we can also cite recent works that
combine failure propagation analysis and timing constraints, such
as~\cite{bittner2016}. This work defines an automatic method for
synthesising \emph{Timed Failure Propagation Graphs} (TFPG), that is
an extension of the notion of cut-sets including information on the
date of events. TFPG provide a condensed representation that is easier
to use than sets of timed cuts.Therefore, it would be interesting to
use this format in our case.

For future work, we plan to adapt our translation to a new version of
the AltaRica language---called AltaRica 3.0, or OpenAltaRica---that
imposes less restrictions on the computation of flow variables. We
also want to apply our approach to more complex industrial use cases,
involving reconfiguration time besides failure detection and
isolation; or even systems with humans and reaction time in the
loop.

%  More generally, the main purpose of our project is to build on
% the results of use cases in order to propose a set of modelling
% guidelines for taking into account time in failure propagation
% analysis.



% AltaRica 3.0 still relies on propagation based variable update, but
% the order in which this
% propagation takes place in determined at execution time, in other
% words, a fix-point is computed. This update scheme extends
% significantly the expressivity of the language, making possible to
% handle looped systems, i.e. systems in which variables depend of
% each other in a circular way, as the order of the updates is left
% free to the modeller. }


% Actual industrial systems embed several elements of complexity, that
% affects the design phase, caused by the diversity of technical issues
% and evaluation criteria coming from different viewpoints.  

% %
% Nevertheless, defining and verifying these properties is critical for
% embedded and real-time systems.  In particular, time information, as
% delays or durations, are the properties that are central in real-time
% systems design and verification: in fact, temporal aspects can be the
% cause of missed failure detections or undesired reactions to (delayed)
% failure propagation. To be able to perform a safety analysis on the
% temporal properties allows to create systems that will operate as
% intended in a real-world environment.
% % Additional benefits from timed and temporal models are the ability
% % to perform formal verification in early development stages, using
% % automated techniques as model-checking.



The use of timed Altarica will help system designers to verify critical properties when time-bounded reactions are required. On the application side, it is central to use formal methods, e.g. model-checking, to validate properly formalized  specifications. Forcing the designer to produce early well formed models during the specification phase yields to have the specifications formalised and pinned down for the next development phases. Then, the validation of those specifications in the model allows to identify behavioral inconsistencies. Espacially, such inconsistencies are difficult to identify in a classical, purely paper-based, specification process. Last, formal verification proves that none of the possible execution scenarios violates the system properties. Such approaches are useful not only for validating an architecture or FDIR strategy once defined, but also for tuning its parameters during the conception phase. Results from the early V\&V of the on-board processes and FDIR design can be fed back into the requirements analysis phase. The contribution of proper (formal) analysis tools to the complex system designs helps in reducing the specification phase, and the early validation of requirements and models. Such extended V\&V toolbox will eventually consent to reduce the time cost of large projects, helping the development of new spacecraft technologies. 


\section{Future Work}





%%  LocalWords:  Dataflow OpenAltaRica

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: