Уперше побудовано алгортим перекладу опису проектованої системи мовою MSC2000 у мережі Петрі та доведено його коректність за допомогою алгебри процесів, а саме - бісмуляційну еквівалентність вхідних MSC діаграм і синтезованої за цими діаграмами мережі Петрі. За цього визначено формальну семантику базового елемента мови MSC2000-<умова>(condition). Розроблено й обгрунтовано оригінальні алгоритми аналізу та верифікації формальної моделі у вигляді мережі Петрі, що використовують метод TSS розв'язання систем лінійних однорідних і неоднорідних діафантових рівнянь над множиною натуральних чисел, а саме: алгоритм верифікації певних властивостей мереж Петрі, зокрема, (структурної обмеженості), L3-живості, досяжності, наявності дедлоків; алгортим побудови S- і T-варіантів мережі Петрі; алгоритм пошуку пасток і тупиків асиметричної мережі Петрі. Рекомендовано здійснювати аналіз зменшеної складності її динамічних властивостей, який має проводитися за допомогою розв'язання рівняння стану. Уперше запропоновано визначення інваріантності властивостей базової моделі як мережі Петрі, яке використовується для створення оригінальної методики пошуку конфліктів функціональностей проектованої системи.

  Завантажити