Abstract: The article presents an algorithm for translation the system, described by MSC document into ordinary Petri Net modulo strong bisimulation. Only the statical properties of MSC document are explored – condition values are ignored (guarding conditions are considered always true) and all loop boundaries are interpreted as <1,inf>. Obtained Petri Net can be later used for determining various system’s properties as statical as dynamic (e.g. liveness, boundness, fairness, trap and mutual exclusion detection). This net regains forth and back traceability with the original MSC document, so detected errors can be easily traced back to the original system. Presented algorithm is implemented as a working prototype and can be used for automatic or semi-automatic detection of system properties. The algorithm can be used for early defect detection in telecommunication, software and middleware developing. The article contains the example of algorithm usage for correction error in producer-consumer system.

Keywords: MSC, Petri Net, model checking, verification, RAD.

ACM Classification Keywords: D.2.4 Software/Program Verification - Formal methods, Model checking

Link:

EXTENDED ALGORITHM FOR TRANSLATION OF MSC-DIAGRAMS INTO PETRI NETS

Sergiy Kryvyy, Oleksiy Chugayenko

http://foibg.com/ijita/vol16/IJITA16-4-p06.pdf