Spinroot

Greetings!

I am currently working with Spin and Modex again to create and verify models of software on embedded systems.
Now, the following Code extract created some problems when it is transformed into a model and afterwards into a verifier:

#define OPVPFACTOR 				4.56522	
#define ADCMAXMV 				320.0
#define ADCMAX 					65535
#define RESISTANCESHUNT 			0.00025	

static const double ADCFACTOR = (ADCMAXMV * 2.0 / (ADCMAX));

int current = 0;
int *currentpointer = &current;

void calc_test () 
{
	int rawADC = 33000;
	*currentpointer = rawADC;

	double conversion;
	conversion = *currentpointer * ADCFACTOR;
	conversion = conversion - ADCMAXMV;
	conversion = conversion / OPVPFACTOR;
	conversion = conversion / RESISTANCESHUNT;
	*currentpointer = (int) conversion;
}

The task of this function is just to perform some transformations regarding the raw digital output of an ADC. Nothing special, and I also don't intend to include this explicit part in my verification, since Spin is not designed to check such computations in great detail. However, this part is still needed in the overall model, so I wanted to transform it with Modex and convert all of it into c_code{}-statements. The functionality of this part should just be exactly like the original C Code.

However, there were some unexpected results regarding the result of the computation. No matter what value I choose for "rawADC", the value within the "current" variable after these statements was always some huge, negative number. After some debugging and experimenting, I found out that the problem lies within the initialisation of the variable "ADCFACTOR": it is supposed to store a static value in a double type based on some pre-defined system values, which is later used in the computation. The right side of the assignment is a formula, and Modex will turn this declaration into the following c_state{}-statement:

 c_state "double  ADCFACTOR " "Global" "((320*2)/65535)"

So far, so good, but now the initialisation of this variable within the verifier pan.c looks like this:

void
globinit(void)
{
	now.ADCFACTOR   =  ((320*2)/65535) ;
	now.currentpointer   =  &(now.current) ;
}

Now, the result of this computation is sadly interpreted as an integer by the compiler, before it is assigned to the double type. Since the value is smaller than 1, this variable will always contain 0, leading to the stated behaviour of the model.
When replacing the right-hand side if the initialisation with the actual value (0.009765774), everything works fine. But I think this won't be the only time that I encounter expressions of this kind, and there may be other unwished consequences due to this way of translating these declarations in c_state{}-blocks.

Now that I wrote everything down here, I noticed that this problem seems extremly specific for this one case, but maybe this is a hint to a small flaw within the detailed workings of Modex and Spin that could occur on other occasions as well.

Thanks for reading!

So long,
- Max

Greetings to all,

I am currently facing a problem with generating an appropriate model of a C program with Modex.
Since most of the C-Code is executed sequential, there is basically just one process that calls different functions, waits for them to return and loops. I would like to model this behaviour as is, meaning I want to put all of the converted C-Code into one single proctype.
In the beginning, I tell Modex in my test harness what functions I want to include and if I want to turn them into certain kinds of processes. By using the '-n' flag, I just get the transformed C-Code without encapsulation and am able to put it somewhere I see fit within the model. The following is an extract from my current test harness:

%D velo_header.h
%X -L voltage.lut -n voltageUpdate
%X -L voltage.lut -n voltageGetAll
%L voltage
  // some specific translations...
voltageGetAll()                      keep
%%
%P
inline voltageGetAll()
{
  #include "_modex_voltageGetAll.pml"
}
inline voltageUpdate () 
{
  #include "_modex_voltageUpdate.pml"
}

init
{
  // some initilaziations...
  do
  :: true -> voltageUpdate()
  od;
}
%%

I want to omit to put all functions of my code into processes, like Modex initialy does, because this creates enourmous overhead and additional side effects. After some research I found the possibiliy to define an 'inline' block, which creates a quite familiar view comparing to function calls in the original C-Code and does not invoke an additional process. My idea is now to put all the imported functions into corresponding inline blocks and keep the function calls of the original code, which should create a process that runs through the code line by line without any unwanted parallelism.
Now, this approach creates new kinds of problems, namely that the local variables of each imported function appear in a struct with a name corresponding to the process (e.g. "Pp_voltageUpdate->...") which is not defined when I use these inline blocks instead of proctypes.
Since I think that using inlines for each function would help me much with my current model extraction process, I would ask if anyone has some ideas how to get around this named problem or if there is an even easier way to get around the each-function-is-a-proctype-topic without changing the actual source code. 

Kind regards.
Max

Greetings again,

while I was looking into the possibilities of using more than one CPU core for my model verification, I came across the following error which occurs every time when I use the following compilation options:

$ spin -a -o3 model
$ gcc -DNCORE=2 -DSEP_STATE -o pan pan.c
$ ./pan -a
shmget shared queues: Invalid argument
pan: check './pan --' for usage details

This happens every time on every model I try, be it one of my own (which could be flawed) but also on the examples from the PROMELA database (e.g. the one with the PLC Control Schedule) or even the little toy-examples within the SPIN directive. 

Maybe someone knows what I am doing wrong here; even after looking through the multicore-manual, I still can't find a flaw. in my commands.

So long,
Max

Greetings again,

while I was busy continuing the modelling and verification of a small software project, I came across an issue regarding the handling of infinite loops and the way SPIN analyses them during a verification run:

Imagine there is an active proctype within a model that simulates an Interrupt service routine which is called by an overflowing hardware timer. This process looks pretty simple in Promela:

active proctype p_SysTick_Handler()
{
     do
     :: true -> c_code { now.countslices++; };
     od;
}

This endless loop should indicate that this global timer (which is used by a small process scheduler) could be incremented at any time during execution. Without the timer changing, the scheduler will not call any more processes and the whole program halts.
In reality, the timer would just be incremented sporadically in between the other software process, while they continue or wait for the next time slice . This is the behaviour i would like to apply to the model, since the way it is now the following issue occurs: If I now want to test for certain properties or accepting states of the rest of the code, this routine is always taken as a counterexample for basically any test, since in the model, this timer can be incremented infinitely often without any progress in the rest of the code. On the contrary, it is also possible that this routine is not called at all and the scheduler loops in an endless idle circle, which should also be excluded in my model.

I tried to filter these possibilities with LTL-formulas that indicate a limit on the timer increments until some progress is made, without success since all SPIN does is find me more counterexamples of my desired behaviour.
I know that SPIN is not designed to verify time-dependant systems, but I still think that this example can work when done right.
Maybe some of you have some ideas on this case.   

If someones wishes to see the whole code, I can post it in here, but I think this would be overcomplicating things; all that is relevant here now is the timer routine that runs in parallel to several other processes.

Thanks in advance for any feedback,
and so long,
Max

Greetings to everyone,

After working with Modex and SPIN for a while, I discovered a strange behaviour when it comes to using the %X command within a test harness.
I want to extract some functions from the C code and turn them into different type of processes within the resulting PROMELA model.

A simple version of my intended use would be the following:

My c-code:

void foo_a () {
	printf("I want to be an active proctype\n");
}

void foo_p () {
	printf("I want to be a passive proctype!\n");
}

void foo_n () {
	printf("I want to be a proctpye without capsulation!\n");
}

My test harness:

%X -p foo_p	// Turn into passive proctype
%X -a foo_a	// Turn into active proctype
%X -n foo_n	// Don't encapsulate into proctype
%L
printf(...	keep
%%
%P
	active proctype p_foo_n () 
	{
		//Some model-based PROMELA code...
		#include "_modex_foo_n.pml"	//Manually wrap into active proctype
	}	
%%

My expectation is that all functions appear as proctypes in the model file: "foo_p" just as an ordinary proctype, "foo_a" as an active proctype and "foo_n" also as an active one, but manually transfered into the proctype "p_foo_n" through the %P command.

After running modex over the test harness (without errors), the model file looks like this:

// Generated by MODEX Version 2.8 - 1 September 2015
// Tue Sep  8 13:08:54 CEST 2015 from test.prx

 active proctype p_foo_n ()
 {
       printf("I want to be a proctpye without capsulation!\n");
;
 }

When I replace the "-n" flag with a "-p" or a "-a" just like the other two functions, everything looks dandy (although not as originally planed):

// Generated by MODEX Version 2.8 - 1 September 2015
// Tue Sep  8 13:04:20 CEST 2015 from test.prx

 active proctype p_foo_n ()
 {
proctype p_foo_n()
{
       printf("I want to be a proctpye without capsulation!\n");
}
 }
proctype p_foo_n()
{
       printf("I want to be a proctpye without capsulation!\n");
}
active proctype p_foo_a()
{
       printf("I want to be an active proctype\n");
}
proctype p_foo_p()
{
       printf("I want to be a passive proctype!\n");
}

I now have a double-capsulation that won't work when I try to use this model as input for SPIN; but all the functions have been turned into proctypes as planed.
So I am wondering why modex ignores the other %X commands when I use the -n flag for this one process?
Is there more to know about this particular flag or is this just a bug within Modex?

Maybe someone here has some ideas or suggestions regarding this. For the meantime, I will try to find a work-around without the use of uncapsulated proctypes.

So long,
Max

Greetings!

Over the past days, I've been trying to get familiar with the workings of formal verification using the model checker SPIN. Since I want to verify code from a larger project written in C, I started looking into the Modex-Tool, which seems to be the state-of-the-art C-to-Promela converter.

Now, after reading carefully through the given instructions and troubleshooting hints on this website, I still have some grave problems of applying the conversion and the following verification on my own C code. Maybe some of you can help me with one of the following problem sources:

-  How do I work with system header files when using Modex? Either the translation fails because of some unknown data types (e.g. "u_int32_t" defined in "types.h") or, when I explicitly include the source of the header file, fails because of numerous syntax errors within the given code of the header. It also seems not wise to always include all the information of the header files, so I am wondering how to tell Modex about the relevant parts of the system header files for my program. The only solution I found so far is to explicitly define the missing information in the test harness (within an %H section). Is there a better way to do this?

- After some experimenting, I was able to convert some of my code into a Promela-model. Also the generating of the model checking code was successful (using "spin -a model"). The problems began when I try to compile the resulting pan.c, which I couldn't do without a great load of errors. It seems that some definitions of my own datatypes (using "typedef") was dropped during one of the conversion steps, and are thus missing in the final pan.c (not all of them for some reason, one even appears two times). When I insert these manually, more errors of undefined references and wrongly defined structures appear, which led me to the conclusion that the conversion from my original code to Promela still inherits some errors, which I am not able to pin down.
To put my question in more general terms: How can I track an error that occurs during the compilation of the model checking code back to  my original code or the translated Promela code? It has been noted in the manual that any errors occurring during the three conversion steps should always be tackled by altering the test harness and not change the results of each phase (e.g. "model" or "pan.c", like I did before); but in my cases, I can't see any connection between the (mostly syntactic) errors of the pan.c file and the options I have when I define my test harness.

Maybe some of you can help me with some hints on the general usage of Modex and SPIN or specifiably by looking at my code and see if you find an explanation of the occuring errors.   
You can see the code for a simple process scheduler in an embedded system below.

Thanks to you in advance,
and so long,

Max

/*	Author: Max Schachtschabel
 *
 *	Stripped-down version of BMS-Software.
 *	
 *	Scheduler 
 */

#include <inttypes.h>
#include <stdio.h>
#include <stdlib.h>

#define MAXPROCS 20							
#define TICKFREQ 1000

#define MAXPROCS 20								
#define TICKFREQ 1000	
#define SCHEDLIST 1		
#define SYNCAMMOUNT 32

typedef void (*functpointer) (void);
typedef struct proc
{
	///process number
	int procnum;
	///pointer to function
	functpointer fpointer;
	///Ticks to periodically skip
	int tickskip;
	///used to store ticks until next run (tickskip + one time offset)
	int noruncount;
	///pointer to next process
	struct proc *next;
	///pointer to previous process
	struct proc *prev;
}process;

uint32_t SystemCoreClock = 72000000;
static const int PROCTIME = 1/TICKFREQ;	
extern volatile int16_t synccounter;
static const int SYNCTICKS = TICKFREQ / SYNCAMMOUNT;	

uint16_t countslices = 0;
uint16_t lastslice = 0;
uint16_t slicelimit = 0;
uint8_t numprocs = 0;
process *plist;
process *lastp;
process *currentproc;

uint16_t systickGetTickbase()
{
	return SystemCoreClock / TICKFREQ;
}


int schedulerCalcMaxTickSkip()
{
	process *indx;
	indx = plist;
	int limit = 0;
	while(indx != NULL)
	{
		if(limit < indx -> tickskip)
		{
			limit = indx -> tickskip;
		}
		indx = indx -> next;
	}
	return limit;
}


int schedulerStart()
{
	uint16_t tickbase;
	int maxtick;

	tickbase = systickGetTickbase();
	maxtick = schedulerCalcMaxTickSkip();
	printf("Processes initialised as: Tickbase: %d, NumProcs: %d\n", tickbase, numprocs);
	if(numprocs == 0) {return 1;}
	slicelimit = 1000;
	printf("MaxTickSkip: %i\n", maxtick);
	//SysTick_Config(systickGetTickbase());
	return 0;
}


void SysTick_Handler (void)	//ISR
{
	countslices++;
}


uint8_t schedulerGetSlice()
{
	return countslices;
}


int schedulerCreateProc(functpointer p, int tickskip, int offset)
{
	if(numprocs >= MAXPROCS) {return 1;}
	process *node;
	node = (process*) malloc(sizeof(process));
	if (node == NULL){return -1;};
	node -> fpointer = p;
	node -> tickskip = tickskip;
	node -> procnum = numprocs;
	node -> next = NULL;
	node -> prev = NULL;
	node -> noruncount = tickskip + offset;
	if(numprocs == 0)
	{
		plist = node;
		lastp = plist;
	}
	else
	{
		lastp -> next = node;
		node -> prev = lastp;
		lastp = node;
	}

	numprocs++;
	return 0;
}


void schedulerRunOneProc()
{
	volatile short slicetaken = 1;
	if (lastslice != countslices)
	{
		slicetaken = 0;
		lastslice = countslices;

		//run process
		process *indx;
		indx = plist;
		while(indx != NULL){
			indx -> noruncount--;
			if(indx -> noruncount <= 0 && slicetaken == 0)
			{
				currentproc = indx;
				indx -> fpointer();
				slicetaken = 1;
				if(indx -> noruncount < -10)
				{
					indx -> noruncount = indx -> tickskip;
				}
				else
				{
					indx -> noruncount = indx -> noruncount + indx -> tickskip;
				}
			}

			indx = indx -> next;

		//place executed process at end of list
			if(slicetaken != 0)
			{
				if(currentproc != lastp && numprocs > 1)
				{
					if(currentproc == plist)
					{
						plist = currentproc -> next;
						plist -> prev = NULL;
					}
					else
					{
						currentproc->prev->next = currentproc ->next;
						currentproc -> next -> prev = currentproc -> prev;
					}
					lastp->next = currentproc;
					currentproc -> prev = lastp;
					currentproc -> next = NULL;
					lastp = currentproc;
				}
			}
		}
	}
}



void schedulerRunProcs()
{
	static short slicetaken = 1;									// variable to store if processes ran this time slice
	///1) Check if new time slice -> then reset slice taken variable
	if (lastslice != countslices)
	{
		///2) Reset slice taken variable to 0
		slicetaken = 0;
		///3) Set lastslice variable to countslices value to detect next time slice
		lastslice = countslices;
		///4) Set process index to start of list
		currentproc = plist;
	}
	///5) Check if processes were already run this time slice
	if(slicetaken == 0)
	{
		///6) Set slice taken variable to 1
		slicetaken = 1;
		///7) Iterate process list until end reached (all following actions per process) - check if time slice has ended
		while(currentproc != NULL && lastslice == countslices)
		{
			///8) Decrement counter for skips of time slices of process
			currentproc -> noruncount--;
			///9) Check if counter for skip reached 0
			if(currentproc -> noruncount <= 0)
			{
				///10) If yes execute function
				currentproc -> fpointer();
				///11) Reset skip variable to tick skip value of process
				currentproc -> noruncount = currentproc -> noruncount + currentproc -> tickskip;
			}
			///12) Move pointer to next process, continue with 8)
			currentproc = currentproc -> next;
		}
		///13) Check if pointer is indexing NULL - else not all processes could be run in time.
		if(lastslice != countslices)
		{
			printf("Process list took longer than time slice! Current slice: %i, last slice: %i\n", countslices, lastslice);
		}
	}
}