Menu
▾
▴
czt-devel
|
From: Cristian V. S. <vid...@ms...> - 2012-08-21 19:09:37
|
Dear. I need to know if Model Checking is possible using CZT? If so, where can I find related information about that? If not, I'd like to be a member of the team for doing a program for Model Checking... I wait for your comments. Sincerely, Cristian. -- Cristian Vidal Silva Computer Engineer Master in Computer Science Ph.D. Student of Michigan State University Chilean Fulbright Scholar |
|
From: Tim M. <tm...@un...> - 2012-08-23 23:48:09
|
Hi Cristian, Leo Freitas did some work on model checking Circus (an extension of Z). He would be the person to talk to about this (if he has not already replied to you). A group at the University of Sheffield also did some work on translating Z to SAL for model checking: http://staffwww.dcs.shef.ac.uk/people/A.Simons/z2sal/ Regards, Tim On 22/08/12 05:09, Cristian Vidal Silva wrote: > Dear. > > I need to know if Model Checking is possible using CZT? If so, where can > I find related information about that? If not, I'd like to be a member > of the team for doing a program for Model Checking... > > I wait for your comments. > > Sincerely, > > Cristian. > |
|
From: Leo F. <leo...@ne...> - 2012-08-24 07:14:23
|
Hi Cristian, Tim is right, there is work on model checking for Circus on my PhD. But not the differences here. First, what do you mean by model checking? If the traditional (SPIN, SMV, etc) temporal logic one, what does this has to do with Z (or how are you linking it with Z)? If you mean refinement model checking (FDR), there is work on Circus for that which involves Z + CSP. I have a paper on a survey of refinement model checking and its use, if that's could be helpful. Also, model checking requires a finite domain (for search), and Z models could be made finite, but aren't usually. The pointer below to Z to SAL is good, and there is also the work of Alexandre Motta, in Brazil, who worked on using FDR to model check a CSP-Z model (something like a precursor to Circus). PS: Thank you for using the list :-) Best, Leo On 24 Aug 2012, at 00:43, Tim Miller wrote: > Hi Cristian, > > Leo Freitas did some work on model checking Circus (an extension of Z). > He would be the person to talk to about this (if he has not already > replied to you). > > A group at the University of Sheffield also did some work on translating > Z to SAL for model checking: > http://staffwww.dcs.shef.ac.uk/people/A.Simons/z2sal/ > > Regards, > Tim > > On 22/08/12 05:09, Cristian Vidal Silva wrote: >> Dear. >> >> I need to know if Model Checking is possible using CZT? If so, where can >> I find related information about that? If not, I'd like to be a member >> of the team for doing a program for Model Checking... >> >> I wait for your comments. >> >> Sincerely, >> >> Cristian. >> > > > ------------------------------------------------------------------------------ > Live Security Virtual Conference > Exclusive live event will cover all the ways today's security and > threat landscape has changed and how IT managers can respond. Discussions > will include endpoint security, mobile security and the latest in malware > threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ > _______________________________________________ > CZT-Devel mailing list > CZT...@li... > https://lists.sourceforge.net/lists/listinfo/czt-devel |
Thanks for helping keep SourceForge clean.
X