What is it?
The latin word "Tutela" stands for "protection". tutela is a software tool that can be used to determine how much protection a computer system has against possible (un)predictable human operator action variations. Before going into details of the software we need to acknowledge our use of the model checker Spin which is used by our system to search for counterexamples. Tutela is built using the java programming language using the Netbeans development framework. Currently it works on UNIX like operating systems. Since it needs to execute shell scripts for interfacing with Spin model checker, it is not portable to the Windows platform.Main features
Tutela needs both the human operators and the computer system to be modeled as a Concurrent Game Structure (CGS).
CGS creation interface
It offers an interface that allows incremental buildup of the CGS representing the combined interactions of computer(s) and human operator(s). This CGS should contain computer response to all possible behavior on part of the humans. After the CGS is created, it is then translated into Promela code which is the input language for the model checker Spin.Proposition set creation interface
A CGS has a set of propositions which may hold true of false in each state. Tutela provides an interface to create this set of propositions. There will be an interface for modification of the propositions in future.
Player action set creation interface
A CGS consists of players whose collaborations cause the structure to transition from state to state. Hence there is a set of possible actions ( we also refer to them as the vocabulary of the players) associated with each player in a CGS. However, in each state, only a subset of the possible actions is enabled for the players. Tutela allows the creation/modification of the list of all possible actions for each player. Currently this interface only supports one computer component referred to as the player named CS and one human component. It will be extended to support creation/modification of vocabulary for a flexible number of players.
Since the current interface is designed with only two players in mind, there is no interface to create the list of players as of now.
State creation interface
Each state in a CGS consists of a label, a set of propositions which are true in that state, subsets of actions available to each player and the transitions that emit from that state. The top-level interface for state creation looks like this.
It allows for adding new states and also deleting already created states. The interface for creating all but the transition component of a state looks as follows:
This interface requires that in each state, each player has the action "noaction" available to them. If the user does not choose this action for a player, then the interface will warn the user and then enable the noaction action for that player by itself. It will also warns users if no propositions are selected to be true in that state.
Transition list creation interface
As seen on the main interface for state creation, users are allowed to enter transitions from already created states. If the user wants to transition to a new state, then the interface will require that at least some information is entered about that new state first using the state creation interface. The user can later on use the state creation interface again to enter transitions for the newly created state.
The transition interface displays the up to date list of states. The display will be cleaned up later on so that the information displayed about each state is more helpful to the users. Currently, this interface also asks for possible context change as a side effect of the transition under consideration etc. These information can be used to translate the CGS to reactive module code suitable for input to the ATL model checker mocha. The translation to mocha input language has been developed separately and has not been integrated into tutela yet. The interface also tries to ensure that the user enters at least one transition each for each possible human action. After the CGS is entered in its entirety, it needs to be translated into a format that can be easily translated into some other language like Promela. Our goal is to allow two possible methods: the user uses the CGS creation interface to create the CGS which then gets translated into a CGS encoding language designed by us which then gets translated into Promela. Or the user encodes the CGS in the CGS encoding language and provides the CGS file directly to the analyzer. Currently the conversion of CGS to an intermediate CGS encoding language does not exist. One function has been developed which allows for loading a CGS that consists of the raw data files obtained from the CGS creation interface. This module currently can handle only two players. On the other hand another module has been developed which can handle any number of players but expects the CGS to be encoded using the CGS encoding language.
CGS thinning interface
Tutela then requires the user to provide their understanding of the guarantees that the computer system provides to the human users and what the computer system considers as reasonable behavior on part of the human operators. These assumptions are then used to thin down the CGS created with the CGS creation interface. The thinning process is performed in a manner such that the resulting CGS is the maximal CGS preserving the aforementioned guarantees. As will be shown in our research papers, this provided a way of reasoning about human operators whose behavior is contained within the boundaries delimited by the assumptions of the computer system. Currently we can execute a thinning algorithm on CGS w.r.t. the protection envelop properties specified using a provided interface.
