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: Mon, 1 Jul 2013 12:29:12 +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<mailto:oyvind.teig at autronicafire.no>
www.autronicafire.no<http://www.autronicafire.no>
www.teigfam.net/oyvind/home/<http://www.teigfam.net/oyvind/home/> (also work-related)

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130701/850ce37c/attachment.html>