LoTuS: uma Ferramenta Gráfica Extensível para Modelagem, Análise e Verificação de Modelos LTS e PLTS

Resumo

Este artigo apresenta LoTuS, uma ferramenta para modelagem gráfica, análise e verificação de comportamento de software usando LTS e PLTS. Suas principais contribuições são: facilitar o processo de modelagem formal através de um mecanismo de drag and drop que permite criar tanto modelos não probabilísticos como probabilísticos; permitir a geração de modelos a partir de outras fontes, como diagramas de sequencia da UML ou rastros de execução; prover um conjunto de técnicas de análise de modelos, como simulação, execução, detecção de deadlock e verificação probabilísticas de propriedades de alcançabilidade; e por fim, fornecer uma API para que desenvolvedores possam adicionar novas funcionalidades através da criação de plugins. A ferramenta foi avaliada em termos de sua usabilidade e desempenho e através de um estudo de caso no qual suas principais funcionalidades foram exercitadas.