Modélisation formelle des systèmes critiques