Model Checking of UML Activity Diagrams Using a Rule-Based Logical Model
Iwona Grobelna, Michał Grobelny, Marian Adamski · Studies in systems, decision and control · 2015
UML activityDiagram (UML) activity diagrams can be used as semi-formal specificationSpecification semi-formal of logic controllerLogic controller behavior. On the other hand, formal methodsFormal method applied at any stage of system development allow increasing in the quality of final products. In the chapter use of the model checkingModel checking technique to validate the specificationSpecification against some specified requirementsRequirements is described. The specificationSpecification is initially expressed by means of UML activity diagramsDiagram (UML) activity and then is transformed to a rule-based logical modelRule-based logical model suitable both for verification purposes and for logical synthesis for FPGAFPGA devices.