Да... Фёдор Васильевич в такой ситуации, пожалуй, сказал бы: "ну, не буду вам мешать"...  А я ещё и помогу... 
На самом деле всё по-видимому намного проще с учётом последних достижений формальной верификации... И получить такое описание, как составляется в предыдущих постах, можно другим путём.
Берём язык моделирования типа Promela и расписываем на нём для каждой роли назначенные (при текущем распределении) техоперации (включая "другую работу" - абстрактно, но чтобы как-то моделировалось переменное время загрузки ею исполнителя), техпроцесс координации этих операций. Ну и не забываем везде передачи между ТО согласно ТП, как его можно извлечь из постановки. Конкретика реализации, как я пока этот язык понял, будет, допустим, в том, что головной процесс модельной программы запускает координаторов всех ролей, передаёт в выбранные процессы какие-то данные... и пошло-поехало...
Далее. Загоняем описание в среду, использующую этот язык как входной (в данном случае, допустим, Spin). Определяем требования-формулы (там, чтобы закончился не позднее или вообще закончился, чтобы все ТО были пройдены, ...) и запускаем в режиме верификации. Среда проверяет модель... и, если реальному аналитику не повезло (а "бизнес-описателю" наоборот ), выдаёт контрпример[ы]. Каждый контрпример - это и будет "бизнес-процесс", хреновый в смысле заданных требований... причём среда выдаёт в графической нотации... так что можно было не рисовать ничего вручную... А представляете, сколько возможно БП, соответствующих конкретным требованиям при конкретном назначении на работы (которое мы отразили включением ТО-процессов в сферу коорд-процесса для конкретного РМ)?.. Для произвольной задачи это только Юрий Глебович Карпов знает, наверное... или Амир Пнуэли...
Но. "Описателя", конечно, только хреновые БП, возможные в данной модели оргсистемы, не устроят. Ему ж надо отчитываться о положительных итогах внедрения...  Тут есть два пути.
Иногда можно поставить задачу моделирования (реальной оргсистемы для данной задачи) так, чтобы верификатор нашёл все возможные решения (соответствующие условиям задачи - которые в требованиях отражаются специальным образом). У Карпова можно видеть пример с переправой волка, козы и капусты. И если предметку можно свести к чему-то такому - то можно и (не без усилий и математической культуры) написать модельную программу и она выдаст варианты. Если нельзя, но очень хочется... то при опять же культуре тоже иногда, видимо, можно... только в этом случае не завидую я винчестеру и/или принтеру, которые будут принимать результаты...
Другой путь - воспользоваться уже режимом симуляции модели. Запустил при конкретных исходных данных - получил схему хода совместно протекающих взаимодействующих процессов - сиди, разбирайся... вышел (в смысле, разобрался) - снова надумал другие данные-запустил-получил-разбирайся... "романтика!"...
Понятно, о чём речь? Какие будут возражения?.. конструктивные опять же...
Кстати, польза от такого моделирования в том, что можно определить процессы вместе с требованиями к ним. Выявив те или иные неопределённости в неформальной постановке задачи (что они у меня есть - я и не сомневался - даже сразу предупредил ). Так что юмор выше к методу проверки моделей не относится... И кстати, уточнения понимания задачи, возникшие по ходу имитации проверки модели, могут оказаться полезными для реального моделирования...
|
