Model‐Based Analysis
Frédéric Boniol, Philippe Dhaussy, Luka Le Roux, Jean-Charles Roger · 2013
This chapter lays out a complementary path, one that relies on modelchecking, allowing to push forward the limits of combinatorial explosion. This path seeks to limit the two sources of complexity: external complexity and internal complexity. The chapter describes the part of the UML-MARTE model that is considered for the transformation in Fiacre language, whose syntax is presented briefly. It focuses on the principle of requirement checking by considering use cases that correspond to the programming models of the pacemaker. Test results are shown for both tools: TINA SELT and OBP Explorer. The technique of reduction via context exploitation, using OBP, is described as well as its implementation in CDL language. The chapter then presents the verification method using both tools, TINA and OBP Explorer. It ends with an assessment and a conclusion. Controlled Vocabulary Terms unified modeling language