Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using frama-c to verify coding patterns of concurrent sw

  • Subject: [Frama-c-discuss] Using frama-c to verify coding patterns of concurrent sw
  • From: Oyvind.Teig at autronicafire.no (Teig, Oyvind CCS)
  • Date: Tue, 2 Jul 2013 11:35:56 +0000
Sirs

I have sw processes (task, thread etc..) as C functions

* They are called by a scheduler, and will be rescheduled to the first line after the descheduling point [1]
* So, scheduling is "cooperative", not preemptive (i.e. the "channel drives the scheduling")
* Local context in each process is allocated on the heap, so state that survive scheduling is stored there
* I have described a couple of patterns that are interesting to verify with frama-C .[2], [3]
* Is it possible to set up an ACSL specification that would be able to verify that certain combinations of local state variables _now_ and certain other combinations _later_ on will sooner or later arrive?
* Even more than that: I will need to verify more than two steps!

[1] - "New ALT for Application Timers and Synchronisation Point Scheduling" at http://www.teigfam.net/oyvind/pub/pub_details.html#NewALT 
[2] -" XCHANs: Notes on a New Channel Type at http://www.teigfam.net/oyvind/pub/pub_details.html#XCHAN 
[3] - "The "knock-come" deadlock free pattern" at http://oyvteig.blogspot.fr/2009/03/009-knock-come-deadlock-free-pattern.html 

Med vennlig hilsen / Best regards

?yvind Teig
Senior utviklingsingeni?r, siv.ing.? / Senior development engineer, M.Sc.
__________________________________________
Autronica Fire and Security AS
UTC CCS EMEA Fire & Security Operations 
Phone: + 47 73 58 24 68 / Mobile +47?959 61 506
E-mail:? oyvind.teig at autronicafire.no???????? 
www.autronicafire.no
www.teigfam.net/oyvind/home/ (also work-related)

Fra: Virgile Prevosto <virgile.prevosto at m4x.org>
Dato: 2. juli 2013 11:46:06 CEST
Til: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
Kopi: "Ogaard, Ommund UTCFS" <Ommund.Ogaard at autronicafire.no>,? ?yvind Teig (oyvind.teig at teigfam.net) <oyvind.teig at teigfam.net>
Emne: Re: [Frama-c-discuss] Using frama-c to verify coding patterns of concurrent sw
Hello,

2013/7/1 Teig, Oyvind ?????????????CCS <Oyvind.Teig at autronicafire.no>:



? ???????Is it possible to set up an ACSL specification that would be able
to verify that certain combinations of local state variables _now_ and
certain other combinations _later_ on will sooner or later arrive?

? ???????Even more than that: I will need to verify more than two steps!

www.teigfam.net/oyvind/home/ (also work-related)

I think that you might be interested by the Aora? plug-in
(http://frama-c.com/aorai.html and
http://amazones.gforge.inria.fr/aorai/), that generate ACSL
specifications from an automaton describing the sequences of function
calls that are authorized for the program. Be aware though that it is
still a quite experimental plug-in. Some extensions might be devised
inside the FP7 project Stance and the ITEA project OpenETCS, but as
usual, we'd be happy to start further collaborations around the
subject.

Best regards,
--
E tutto per oggi, a la prossima volta
Virgile

-------------------------------------------------------
(I only received digest and not reply at this address.. Is this subscription list framework really only mail based?)
I tried to regenerate the thread by hand.

Dear Virgile

What you are describing is interesting! 

Q1. What is not supported? 

It looked like the "safety" (state) part is present, not the temporal things. Which would probably be ok. I am only after verifying that a software pattern is kept.

Between every state that I want to check, any number of calls (=schedule) may be done, and they would side effect into the preconditions of the test. Some message would arrive on a channel (a call into the function (process)) or some timeout (the same) would cause the state changes that will trigger some code that I want to verify. A temporal requirement may be "eventually", it must be possible to detect if bad coding causes entering a certain state as not possible, i.e. "not eventually". 

Q2. Do you think this is possible?

Q3. What's the state of the Promela interface?

Med vennlig hilsen / Best regards

?yvind Teig
Senior utviklingsingeni?r, siv.ing.  / Senior development engineer, M.Sc.
__________________________________________
Autronica Fire and Security AS
UTC CCS EMEA Fire & Security Operations 
Phone: + 47 73 58 24 68 / Mobile +47 959 61 506
E-mail:  oyvind.teig at autronicafire.no         
www.autronicafire.no
www.teigfam.net/oyvind/home/ (also work-related)