1
<html xmlns:v="urn:schemas-microsoft-com:vml"
2
xmlns:o="urn:schemas-microsoft-com:office:office"
3
xmlns:p="urn:schemas-microsoft-com:office:powerpoint"
4
xmlns="http://www.w3.org/TR/REC-html40">
7
<meta http-equiv=Content-Type content="text/html; charset=windows-1252">
8
<meta name=ProgId content=PowerPoint.Slide>
9
<meta name=Generator content="Microsoft PowerPoint 9">
10
<link id=Main-File rel=Main-File href="../slides2.htm">
11
<link rel=Preview href=preview.wmf>
14
v\:* {behavior:url(#default#VML);}
15
o\:* {behavior:url(#default#VML);}
16
p\:* {behavior:url(#default#VML);}
17
.shape {behavior:url(#default#VML);}
18
v\:textbox {display:none;}
21
<title>Developing a Framework for Simulation, Verification and Testing of SDL
22
Specifications</title>
23
<meta name=Description content="3-Nov-00: Activator">
24
<link rel=Stylesheet href="master03_stylesheet.css">
29
width:6.0in !important;
30
height:4.5in !important;
31
font-size:107% !important;}
34
<script src=script.js></script><script><!--
36
if( !IsNts() ) Redirect( "PPTSld", gId );
38
</script><!--[if vml]><script>g_vml = 1;
39
</script><![endif]--><script for=window event=onload><!--
40
if( !IsSldOrNts() ) return;
41
if( MakeNotesVis() ) return;
45
</script><![endif]><o:shapelayout v:ext="edit">
46
<o:idmap v:ext="edit" data="10"/>
50
<body lang=EN-US style='margin:0px;background-color:white'
51
onclick="DocumentOnClick()" onresize="_RSW()" onkeypress="_KPH()">
53
<div id=SlideObj class=sld style='position:absolute;top:0px;left:0px;
54
width:534px;height:400px;font-size:16px;background-color:white;clip:rect(0%, 101%, 101%, 0%);
55
visibility:hidden'><p:slide coordsize="720,540"
56
colors="#FFFFFF,#000000,#808080,#000000,#00CC99,#3333CC,#CCCCFF,#B2B2B2"
57
masterhref="master03.xml">
58
<p:shaperange href="master03.xml#_x0000_s1025"/><![if !ppt]><p:shaperange
59
href="master03.xml#_x0000_s1028"/><p:shaperange
60
href="master03.xml#_x0000_s1029"/><![endif]><p:shaperange
61
href="master03.xml#_x0000_m1026"/><v:shape id="_x0000_s10242" type="#_x0000_m1026"
62
style='position:absolute;left:54pt;top:14.5pt;width:612pt;height:60pt'>
63
<v:fill o:detectmouseclick="f"/>
64
<v:stroke o:forcedash="f"/>
65
<o:lock v:ext="edit" text="f"/>
66
<v:textbox style='mso-fit-shape-to-text:t'/>
67
<p:placeholder type="title"/></v:shape><p:shaperange
68
href="master03.xml#_x0000_m1027"/><v:shape id="_x0000_s10243" type="#_x0000_m1027"
69
style='position:absolute;left:27pt;top:89.25pt;width:666pt;height:442pt'>
70
<v:fill o:detectmouseclick="f"/>
71
<v:stroke o:forcedash="f"/>
72
<o:lock v:ext="edit" text="f"/>
73
<v:textbox style='mso-fit-shape-to-text:t'/>
74
<p:placeholder type="body" position="1"/></v:shape>
75
<div v:shape="_x0000_s10242" class=T style='position:absolute;top:3.25%;
76
left:8.42%;width:83.14%;height:10.0%'>Activator</div>
77
<div v:shape="_x0000_s10243" class=B><span style='position:absolute;
78
top:17.25%;left:8.42%;width:102.43%'><span style='font-size:88%'><span
79
style='mso-special-format:bullet;position:absolute;left:-3.65%'>�</span></span><span
80
style='font-size:88%'>SDL differentiates between process definition and </span></span><span
81
style='position:absolute;top:23.5%;left:8.42%;width:86.89%'><span
82
style='font-size:88%'>process instance </span></span>
83
<div style='position:absolute;top:31.0%;left:4.68%;width:90.63%;height:6.5%'><span
84
style='position:absolute;top:0%;left:4.13%;width:95.86%'><span
85
style='font-size:88%'><span style='mso-special-format:bullet;position:absolute;
86
left:-4.31%'>�</span></span><span style='font-size:88%'>Defined process
87
activation mechanism </span></span></div>
88
<div style='position:absolute;top:38.25%;left:4.68%;width:90.63%;height:6.5%'><span
89
style='position:absolute;top:0%;left:4.13%;width:95.86%'><span
90
style='font-size:88%'><span style='mso-special-format:bullet;position:absolute;
91
left:-4.31%'>�</span></span><span style='font-size:88%'>Receiver process
92
instance </span></span></div>
93
<div style='position:absolute;top:45.5%;left:4.68%;width:90.63%;height:5.75%'><span
94
style='mso-special-format:nobullet;display:none'>�</span><span
95
style='font-size:75%'><span style='mso-tab-count:1;width:4.13%'> </span></span><span
96
style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b>(1
97
receiverprocess start </b></span></div>
98
<div style='position:absolute;top:52.0%;left:4.68%;width:90.63%;height:4.5%'><span
99
style='mso-special-format:nobullet;display:none'>�</span><span
100
style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
101
style='mso-tab-count:1;width:4.13%'> </span><span style="mso-spacerun: yes">�
102
</span>((ackid . nil) (frameid . nil) (self . 1) </b></span></div>
103
<div style='position:absolute;top:57.5%;left:4.68%;width:100.74%;height:4.5%'><span
104
style='mso-special-format:nobullet;display:none'>�</span><span
105
style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
106
style="mso-spacerun: yes">� </span><span style='mso-tab-count:1;width:.41%'> </span><span
107
style="mso-spacerun: yes">���</span>(sender . nil) (parent . 0) (offspring .
108
nil) </b></span></div>
109
<div style='position:absolute;top:62.75%;left:4.68%;width:90.63%;height:4.5%'><span
110
style='mso-special-format:nobullet;display:none'>�</span><span
111
style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
112
style="mso-spacerun: yes">��� </span>((start �)) nil) </b></span></div>
113
<span style='position:absolute;top:68.25%;left:8.42%;width:95.5%'><span
114
style='font-size:88%'><span style='mso-special-format:bullet;position:absolute;
115
left:-3.92%'>�</span></span><span style='font-size:88%'>Correctness property:
116
defined a recognizer for </span></span><span style='position:absolute;
117
top:74.5%;left:8.42%;width:86.89%'><span style='font-size:88%'>valid instances
118
of a system </span></span>
119
<div style='position:absolute;top:81.5%;left:4.68%;width:90.63%;height:5.75%'><span
120
style='mso-special-format:nobullet;display:none'>�</span><span
121
style='font-size:75%'><span style='mso-tab-count:1;width:4.13%'> </span></span><span
122
style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b>(defthm
123
activate-makes-instance </b></span></div>
124
<div style='position:absolute;top:88.25%;left:4.68%;width:90.63%;height:4.5%'><span
125
style='mso-special-format:nobullet;display:none'>�</span><span
126
style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
127
style='mso-tab-count:1;width:4.13%'> </span><span style="mso-spacerun: yes">�
128
</span>(implies (wf-type S) </b></span></div>
129
<div style='position:absolute;top:93.5%;left:4.68%;width:90.63%;height:4.5%'><span
130
style='mso-special-format:nobullet;display:none'>�</span><span
131
style='font-family:"Courier New";font-size:63%;color:#5F5F5F'><b><span
132
style="mso-spacerun: yes">������������ </span>(wf-instance (activate S) S)))</b></span></div>