LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Tin tức » Nghiên cứu sinh

THIERRY-MIEG Yann

Tiến sĩ
Nhóm nghiên cứu : MoVe
Giảng viên có bằng tiến sĩ khoa học
Ban lãnh đạo nghiên cứu : Fabrice KORDON
Đồng hướng dẫn : ILIÉ Jean-Michel

Techniques for Model-checking of high-level specifications

The increasing complexity of distributed applications makes their dependability a problematic issue. Model-checking is a formal method for automatically validating a system, based on an exhaustive exploration of its behaviors, but that is challenged by the combinatorial state-space explosion problem. To address this problem, we propose an approach based on automatic symmetry analysis of models and of properties expressed in Linear Temporal Logic (LTL), allowing construction of a quotient state graph that supports verification. We combine this approach with symbolic representations, thus offering an extremely compact storage solution. We define a flexible hierarchical decision diagram model, that allows to efficiently exploit a compositional description of a system. Finally, we place our techniques within a model-based rapid application development methodology, to allow their use in an industrial context.
Bảo vệ luận án : 13-12-2004 - 10h - Site Scott - salle C.044
Hội đồng giám khảo :
S. Haddad (Univ paris 9) Rapporteur
S. Donatelli (Univ. Turin) [Rapporteur]
A. Boujjani (Univ. Paris 7)
J-M. Couvreur (Univ. Bordeaux 1)
J-M. Ilié (Univ Paris 5)
L. Petrucci (Univ. Paris 13)
F. Kordon (Univ. Paris 6) [Directeur]

4 Tiến sĩ 2009 - 2013

Bài báo khoa học 2002-2020

 Mentions légales
Sơ đồ site |