A New Models Editor for the Ivy Workbench

Abstract

Para que as interfaces de sistemas críticos possuam um nível de qualidade que permita o seu uso em segurança, devem passar por um processo rigoroso de análise. A verificação formal de interfaces é uma das formas de realizar essa análise. Para tal, é importante que os desenvolvedores dessas interfaces consigam editar e criar os modelos que acharem mais adequados para as suas interfaces. Tanto os desenvolvedores mais experientes como os menos experientes. A Ivy Workbench é uma ferramenta que permite descrever o funcionamento das interfaces e verificar propriedades sobre o seu comportamento, de forma a identificar potenciais problemas na interação. Deste modo, fornece informação relevante para os desenvolvedores que utilizem o Ivy, para que se possa melhorar o software sem ter de necessariamente passar por um processo de teste manual longo e exaustivo.

O atual editor do Ivy é difícil de manter e não fornece ajuda suficiente nem guia novos utilizadores adequadamente. Por isso, é necessário que haja uma melhor forma de editar os modelos na linguagem Model Action Logic (MAL), a linguagem de programação da Ivy Workbench. O objetivo desta dissertação é construir uma solução que permita que todos os tipos de desenvolvedores consigam construir os seus modelos através de orientações do próprio editor. É bastante desafiante desenvolver uma solução deste gênero, que permita alcançar o nível de apoio pretendido, dado que precisamos de ter em conta com o que é que os utilizadores estão mais confortáveis e quais as ferramentas que usam com maior regularidade, para que seja possível desenvolver uma solução o mais abrangente possível.

Para que se concretize o principal objetivo, enquanto também se alcança o máximo número de utilizadores, optou-se por desenvolver uma extensão de VS Code. Trata-se do editor de código mais utilizado e fornece várias ferramentas para desenvolvedores de extensões, assim como uma vasta documentação. É possível tirar partido das funcionalidades que esta ferramenta já apresenta, típicas de um Integrated Development Environment (IDE) comum, que nos permitem criar novas formas para os utilizadores da Ivy escreverem modelos MAL, e fazendo isso, aumentar a sua produtividade.

Depois da extensão estar concluída, é expectável que esta solução seja mais fácil de manter no futuro, e mais utilizadores achem esta nova solução menos complexa para trabalhar, levando a que estes se sintam mais satisfeitos a utilizar a ferramenta e a própria linguagem, ajudando assim o crescimento da utilização da Ivy Workbench assim como da qualidade do software.

Alternate abstract:

In order for the interfaces of critical systems to have a quality level of security that allows for its safe usage, they should be subject to rigorous analysis process. Formal verification is one of the alternatives to perform that analysis. So, it is important that developers can edit or create the models which they find the most suitable for their interfaces. Both the most experienced developers as well as the least ones. The Ivy Workbench is a tool that allows for the modeling of user interfaces, and for properties about the interface behaviour to be verified, so that potential problems in the interaction can be identified. By doing this, it provides information for the developers who use Ivy, so that their software can be enhanced without having to perform extensive manual testing.

Ivy’s current editor is difficult to maintain, and does not provide enough help nor guidance to inexperienced users. So, there is the need of a better way for users to write in the MAL language, the modeling language of the Ivy Workbench. The goal of this thesis is to build a solution that allows every level of developer to build their own models based on guidance by the editor itself. It can be challenging to put together an editor or code editor extension that would allow such goal, because there is the need to con sider what the users are comfortable with, and what their most often used tools are, in order to build the more embracing solution.

In order to achieve the main goal, while also reaching as many users as possible, it was considered that the best option would be to develop a VS Code extension. VS Code is the most widely used code editor and provides various tools for extension developers, with a vast documentation about their development. Also, it is possible to make use of the features this code editor already presents, common amongst the most used IDE, to build new ways for the users to write MAL, and in doing so, increase their productivity.

After the extensions is completed, it is expected that this new solution will be easier to maintain in the future, and that more users will find it less complicated to work with, leading users to get more satisfied when using the editor and the language itself, thus helping the growth of Ivy Workbench as well as the quality of the software.