Specification of external system behaviour based on D-nets: theoretical aspects and computer tools

A special subclass of coloured Petri nets (so-called D-nets) is presented in the paper. The concept is based on coloured Petri nets (CP-nets [2]) but special structure of such D-nets allows carrying out very interesting formal analysis. The main advantage of the D-nets is possibility of efficient verification of system requirements, i.e., elimination of ambiguity, inconsistency and incompleteness. Such a specification of requirements is prepared as a decision table with rules patterns and then it is transformed into a D-net and computer software is used for automatic verification of its properties. The relevant definitions and main properties of D-nets are presented, and main features of ADDER tool software designed for D-nets analysis are put forward.

---

W artykule przedstawiona została podklasa kolorowanych sieci Petriego, tzw. D-sieci. Pojęcie bazuje na kolorowanych sieciach Petriego, ale specyficzna struktura D-sieci pozwala na przeprowadzenie formalnej analizy reprezentowanej przez nie specyfikacji zachowania się systemu. Główną zaletą D-sieci jest możliwość efektywnej weryfikacji specyfikacji wymagań, tj. eliminacji dwuznaczności, niezgodności i niezupełności. Specyfikacja wymagań jest przygotowywana jako tablica decyzyjna zawierająca szablony reguł decyzyjnych, a następnie jest transformowana do postaci D-sieci i automatycznie analizowana z wykorzystaniem odpowiednich narzędzi komputerowych. W artykule przedstawione zostały definicje podstawowych pojęć dotyczących D-sieci oraz główne cechy systemu ADDER - rozwijanego oprogramowania , którego jedną z możliwości jest analiza D-sieci.