Introduction to Murphi3.1 - I

In software engineering, we have to go through three main stages, formal specification (i.e., that is fully specifies how the models works including all possible exceptions and errors), verification (i.e., verify the specified model, against different inputs and make sure the model works correctly), implementation (i.e., implementing the actual model which is already specified and verified). For detailed understanding click this link.

Murphi3.1

Murphi is a tool that developed to verify whether the specfied model work without any failure (note, this different from error and exception, this is some thing that let the system to unrealistic states. e.g. In a master-slave model, having two master is unrealistic).

Basic Tutorials

In this first post, I mainly focus on providing a basic introduction how to work with murphi3.1, like setting constants, types and variables, and incoming up posts I will go in deep with murphi3.1.

Setting Constants

Constants are analogs to the constants we define in normal programming languages. We use constants to define some strict parameters or limitations in the systems. e.g. Number of Slaves (in master-slave model)

We can set simple constants using following syntax in Murphi,

const
  <constant_name>: <const_value>;

Defining Variables

Again, variables are used to keep track of varying values in the system. We can use either simple variables with exist variable types such as boolean or we can define a custom variables by defining the type in type definition (in that case type definition should presents before defining the variables other wise compilation error would occurs). You can also define the variable as array of varriable by usingarray key word.

Variable can be defined in the following format

Simple definition,

var
	<variable_name>: <type>;

Using array definition,

var
	<variable_name>: array[<type_name_1>] of <type_name_2>;

where type_name_1 is mostly from the type defined upon scalerset or multiset, where as type_name_2 can be from simple complex structured type as well as simple types. I will discuss more about types in the next paragraph.

Defining Types

Next, we look into how to define a type. It can go through either simple steps using predefine structures on top of existing types like scalarset or multiset, or define with enumeration enum. In more complex cases one or more type can be provided as the attributes of the type.

Types can be defined in the following format

Simple Definition: Here the type is define on top of the scalerset.

type
  	<type_name>: scalarset(<integer_value>);

Complex Structure:

In complex structure, we can combine on or more simple types and complex ones as well. Also we can provides enumerations as attributes. Types can be resembles the object of the general programming. In the below examples we can observe that there are two attributes inside the main type (record) such as enum and another one, it can be either another type we defined or predefined types.

type
	<type_name>: record
		<attribute_1>: enum { 
			ENUM_VAL_1,
			ENUM_VAL_2
		};
		<attribute_2>: <type_name>;
	end;

Defining Functions or Procedures.

We can defines functions or procedures based on the following syntax,

procedure NameOfProcedure(<arg_name>: <arg_type>;...);
begin
....
end

You can define input mutliple input arguments by seperating each argument definition using ;.

In the next post, I will discuss on how to define the rulesets, startstate and invariants.

Hope you enjoy this post.