Mihaela Sighireanu's Research Activities
My research domain is about the application of formal methods to the development of complex systems, whatever their nature (hardware, software, or telecom).
More precisely, my interests are in:
- Modelling, specification, and formal analysis of computer systems.
- Modelling of infinite state systems using extended automata (with counters, stacks, clocks).
- Algorithms for verification of models with finite or infinite size (model-checking).
- Software verification.
- Semantics of programming languages.
- Process algebra (CCS, CSP, LOTOS, E-LOTOS).
Other pages describing my research activities:
- my resume,
- a list of publications,
- research projects I'm participating:
- past research projects I've been member:
ACI Jeunes Chercheurs (2002-2005),
- activity report of LIAFA (in french),
- my old home page at VASY team of INRIA.
- Verification of programs with dynamic data structures:
- Verification of concurrent boolean programs with recursive procedure calls and rendez-vous communication: Spade tool.
- Verification of concurrent boolean programs with restricted communication: Press tool.
Model Checking: Finite and Infinite Systems
- Verification of colored Petri nets (or rewriting systems with data). Application to verification of mutual exclusion protocols: CMRS tool.
- Symbolic analysis of extended automata using TReX tool.
TReX does symbolic reachability on products of automata extended with counters and clocks, and communicating by lossy FIFO-channels.
- Contributor member to the CADP toolbox.
- Applying model checking to verify protocols:
- Regular alternation-free mu-calculus used for robotics systems (in French) specified using ORCCAD.
- Using TGA and Uppaal for deriving temporal plans.
- STNU strategies for TGA.
Fault Tolerance for Real-Time Embedded Systems
This work has been done during my Post-doctoral period in the TOLERE project.
Specification Languages for Parallel Systems: Semantics and Compilation
During my thesis, I developed a new language, called LOTOS NT, for the description of communication protocols. This language is an improvement of the LOTOS language, a process algebra based language. I also developed a compiler for LOTOS NT, called TRAIAN, which aims to translate LOTOS NT to an automata model in order to model check the description.
a new value-based asynchronous specification language for concurrent systems.
- Contributor member of RSI (Romanian Institute for Standardization) at
Enhancement to LOTOS Working Group of ISO.
- TRAIAN: an E-LOTOS compiler designed using SYNTAX/FNC2
- An Emacs mode for LOTOS specifications is available here.
- Compilation of abstract data types (in french).
Last modified: Tue Apr 10 10:29:21 CEST 2015
Back to Mihaela's Home Page