Spinroot

A forum for Spin users

You are not logged in.

#1 2015-08-31 09:46:52

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

Modex, Spin and a small C-Project

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);
		}
	}
}

Last edited by Schachtschabel (2015-08-31 10:34:07)

Offline

#2 2015-09-01 05:43:46

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Modex, Spin and a small C-Project

it can be difficult to overcome the initial errors
i will take a look to see if i can advice a general strategy

Offline

#3 2015-09-01 11:48:48

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

Re: Modex, Spin and a small C-Project

That sounds great!

I am in general very interested in the way that SPIN and Modex use Model extraction and automata-based verification and would like to learn the correct usage of these tools. I plan to use this knowledge to look further into the research of combined Hard- and Software-Verification, and I am very glad that such a powerful verification tool like SPIN exists as open-source project.

While I was looking through the papers and articles about SPIN, I found a small publication about a tutorial on "Effective Bug Hunting with Spin and Modex" (during the 12th international SPIN workshop in 2005).
I am guessing that this event could have helped me a lot with my current problems^^
Maybe there exists some documentation about this particular tutorial?

Offline

#4 2015-09-01 20:54:59

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Modex, Spin and a small C-Project

updated files sent by email

Offline

Board footer

Powered by FluxBB