Требуется инструмент для получения спецификации линейной временной логики из диаграммы последовательности UML 2.0

Я работаю над проверкой согласованности модели программного обеспечения. для этого мне нужно написать линейную временную логику для диаграммы последовательности UML 2.0. если у какого-либо органа есть какой-либо другой инструмент для того же, пожалуйста, ответьте как можно скорее. Я буду вам очень обязан. Я нашел очаровательный инструмент с плагином для того же. Есть ли у кого-нибудь исходный код инструмента charmy (проверка согласованности архитектурной модели). На их сайте его нет.

Заранее спасибо.


logic uml formal-verification formal-methods sequence-diagram
person kingh    schedule 18.05.2010    source источник
comment
Существует множество инструментов для преобразования и проверки моделей, когда речь идет о UML. Не могли бы вы дать ссылку на эту линейную темпоральную логику? Я понятия не имею, что это такое.   -  person Gabriel Ščerbák    schedule 18.05.2010
comment
В основном он используется для доказательства свойств безопасности и живучести системы. Здесь я даю две ссылки: 1. en.wikipedia.org/wiki/Linear_temporal_logic 2. < a href="http://www.di.univaq.it/pellicci/download.php?fileID=26" rel="nofollow noreferrer">di.univaq.it/pellicci/download.php?fileID=26   -  person kingh    schedule 19.05.2010
comment
Дубликат stackoverflow.com/questions/2715239/   -  person Charles Stewart    schedule 21.05.2010
comment
@Чарльз Стюарт: этого вопроса больше не существует (больше?).   -  person Gumbo    schedule 23.05.2010
comment
@Gumbo: он был объединен? Я проверял ссылку, когда писал комментарий.   -  person Charles Stewart    schedule 23.05.2010
comment
@Charles Stewart: Эта ссылка точно не работает.   -  person RD1    schedule 30.07.2010

Ответы (2)


arrow_upward
2
arrow_downward

Модель диаграммы последовательности для меня непригодна.

Я имею в виду, что у вас может быть диаграмма последовательности, но базовая модель действительно запутана. Диаграмма последовательности — единственная диаграмма UML, модель которой нельзя использовать повторно. Извините за этот пост, но я думаю, что диаграмма последовательности должна оставаться графической, потому что метамодель не была хорошо разработана в спецификации UML, и уже слишком поздно ее менять!!

person Community    schedule 18.05.2010
comment
Может быть, еще не поздно: drdobbs.com/architecture-and-design / - person Gabriel Ščerbák; 19.05.2010

arrow_upward
0
arrow_downward

Я не уверен, что понимаю проблему. Согласно статье в Википедии, диаграмма последовательности не имеет циклов, поэтому соответствующая формула LTL не будет содержать никаких алмазов или коробок и т. д., это будет просто последовательность атомарных событий, не так ли?

Не могли бы вы предоставить примерную диаграмму последовательности и соответствующую формулу LTL?

person aioobe    schedule 07.05.2010
comment
Вы неправильно прочитали. ibm.com/developerworks/rational/library/3101.html указывает возможны чередование и зацикливание. - person Donal Fellows; 21.05.2010
comment
Кроме того, даже с простым кодом по-прежнему будет необходимо хорошее разбрызгивание ◇ символов; вы не можете рассчитывать на то, что события из диаграммы последовательности происходят немедленно, поэтому в конечном итоге это полезный модальный оператор. (Боже, я начинаю кое-что вспоминать…) - person Donal Fellows; 21.05.2010