[sae-aadl] DDD.aadl finally pushed through BLESS proof checker to generate 998 theorems

[Brian R Larson]

Bruce,

Now I have something significant to report:  DDD.aadl was finally pushed through BLESS proof checker to generate 998 theorems.

Since Toulouse, my goal has been to prove correctness of dual-chamber pacing, DDD mode.  

Achieving this has been much more difficult than I thought.  The proof engine roughly doubled in size.  33 ANTLR3 grammars are now used.  Most grammars are very short.  

The BLESS program proved correct:
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DDD.aadl
Type: application/octet-stream
Size: 16709 bytes
Desc: not available
Url : https://lists.sei.cmu.edu/mailman/private/sae-aadl/attachments/20101016/2cc97d67/attachment-0003.obj 
-------------- next part --------------


The same program transformed into BA+:
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DDD.aadl to BA
Type: application/octet-stream
Size: 3280 bytes
Desc: not available
Url : https://lists.sei.cmu.edu/mailman/private/sae-aadl/attachments/20101016/2cc97d67/attachment-0004.obj 
-------------- next part --------------

(The standard BA annex language does not have port lists in timeout dispatch conditions.)

The 998-theorem proof of DDD.aadl correctness:
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DDD.aadl proof
Type: application/octet-stream
Size: 664789 bytes
Desc: not available
Url : https://lists.sei.cmu.edu/mailman/private/sae-aadl/attachments/20101016/2cc97d67/attachment-0005.obj 
-------------- next part --------------


I'll make up, and send to Peter, a few slides summarizing progress since May.


--Brian



On Oct 15, 2010, at 2:07 PM, Lewis, Bruce (AMRDEC) wrote:

> Classification: UNCLASSIFIED
> Caveats: NONE
> 
> Dear presenters for the AADL meeting, 
> 
> Please send your presentations in advance so Peter and I can have them
> before the meeting.  Send to phf at sei.cmu.edu
> 
> Thanks,
> Bruce
> 
> -----Original Message-----
> From: Lewis, Bruce (AMRDEC) 
> Sent: Thursday, October 14, 2010 10:56 PM
> To: sae-aadl at lists.sei.cmu.edu; sae-aadl-users at lists.sei.cmu.edu
> Cc: Kirstie L Bellman; j.bergmann at opengroup.org; Junkyo (Jack) Fujieda;
> Sha, Lui Raymond; Jose Meseguer; Nam, Min Young
> Subject: Telecon info and updated agenda for Oct 18-21 (UNCLASSIFIED)
> 
> Classification: UNCLASSIFIED
> Caveats: NONE
> 
> Dear all,
> 
> 1. I've attached an updated agenda, see changes to Wednesday afternoon
> and Thursday morning.  Please check, especially if you are presenting
> during those times.
> 
> 2. I've also attached the info for the web meetings.  Remember that you
> can just use the audio on your computers but there is also a toll free
> phone line.  The meeting will open up at 9:45 so we can all get signed
> in before 10:00.
> 
> 
> 3. You can check your system for compatibility and set up by clicking on
> the following link:
> 
> https://sae.webex.com/mw0304l/mywebex/default.do?siteurl=sae&service=1
> 
> you can do this anytime before the meeting / training to see if your
> computer will work.
> 
> 4. From Thierry Cornilleau tests:
> I was able to test successfully flash and quick time, but I wasn't able
> to see the windows media file despite the installation of the Flip4 WM
> plug-in (version 2.3.4.1).
> 
> Looking forward to a great meeting!
> 
> Bruce
> 
> Classification: UNCLASSIFIED
> Caveats: NONE
> 
> 
> 
> Classification: UNCLASSIFIED
> Caveats: NONE
> 
> 
>