%!PS-Adobe-1.0
%%Title: report-020-predict.mss
%%DocumentFonts: (atend)
%%Creator: Dianne King and Scribe 6(1600)
%%CreationDate: 28 June 1988 15:45
%%Pages: (atend)
%%EndComments
% PostScript Prelude for Scribe.
/BS {/SV save def 0.0 792.0 translate .01 -.01 scale} bind def
/ES {showpage SV restore} bind def
/SC {setrgbcolor} bind def
/FMTX matrix def
/RDF {WFT SLT 0.0 eq
{SSZ 0.0 0.0 SSZ neg 0.0 0.0 FMTX astore}
{SSZ 0.0 SLT neg sin SLT cos div SSZ mul SSZ neg 0.0 0.0 FMTX astore}
ifelse makefont setfont} bind def
/SLT 0.0 def
/SI { /SLT exch cvr def RDF} bind def
/WFT /Courier findfont def
/SF { /WFT exch findfont def RDF} bind def
/SSZ 1000.0 def
/SS { /SSZ exch 100.0 mul def RDF} bind def
/AF { /WFT exch findfont def /SSZ exch 100.0 mul def RDF} bind def
/MT /moveto load def
/XM {currentpoint exch pop moveto} bind def
/UL {gsave newpath moveto dup 2.0 div 0.0 exch rmoveto
setlinewidth 0.0 rlineto stroke grestore} bind def
/LH {gsave newpath moveto setlinewidth
0.0 rlineto
gsave stroke grestore} bind def
/LV {gsave newpath moveto setlinewidth
0.0 exch rlineto
gsave stroke grestore} bind def
/BX {gsave newpath moveto setlinewidth
exch
dup 0.0 rlineto
exch 0.0 exch neg rlineto
neg 0.0 rlineto
closepath
gsave stroke grestore} bind def
/BX1 {grestore} bind def
/BX2 {setlinewidth 1 setgray stroke grestore} bind def
/PB {/PV save def newpath translate
100.0 -100.0 scale pop /showpage {} def} bind def
/PE {PV restore} bind def
/GB {/PV save def newpath translate rotate
div dup scale 100.0 -100.0 scale /showpage {} def} bind def
/GE {PV restore} bind def
/FB {dict dup /FontMapDict exch def begin} bind def
/FM {cvn exch cvn exch def} bind def
/FE {end /original-findfont /findfont load def /findfont
{dup FontMapDict exch known{FontMapDict exch get} if
original-findfont} def} bind def
/BC {gsave moveto dup 0 exch rlineto exch 0 rlineto neg 0 exch rlineto closepath clip} bind def
/EC /grestore load def
/SH /show load def
/MX {exch show 0.0 rmoveto} bind def
/W {0 32 4 -1 roll widthshow} bind def
/WX {0 32 5 -1 roll widthshow 0.0 rmoveto} bind def
%%EndProlog
%%Page: 0 1
BS
0 SI
14 /Times-Bold AF
22065 17138 MT
(Predicting Computer Behavior)SH
12 /Times-Roman AF
27570 20841 MT
(Donald I. Good)SH
11 SS
18144 29555 MT
(Technical Report 20)SH
18144 XM
(Technical Report 20)SH
39573 XM
(May 1988)SH
39573 XM
(May 1988)SH
10 SS
26167 52926 MT
(Computational Logic Inc.)SH
26014 54484 MT
(1717 W. 6th St. Suite 290)SH
27167 56042 MT
(Austin, Texas 78703)SH
28195 57600 MT
(\050512\051 322-9951)SH
19440 61385 MT
(This work was)
21 W( sponsored in part by the Defense Advanced)20 W
19440 62490 MT
(Research Projects Agency under ARPA Orders 6082)
129 W( and)130 W
19440 63595 MT
(9151. The)
1087 W( views and conclusions contained in this)418 W
19440 64700 MT
(document are those of)
365 W( the author and should not be)366 W
19440 65805 MT
(interpreted as representing the official)
401 W( policies, either)400 W
19440 66910 MT
(expressed or implied, of Computational Logic, Inc., the)224 W
19440 68015 MT
(Defense Advanced Research Projects)
122 W( Agency or the U.S.)121 W
19440 69120 MT
(Government.)SH
ES
%%Page: 0 2
BS
0 SI
13 /Times-Bold AF
28433 8071 MT
(Abstract)SH
10 /Times-Roman AF
9504 12357 MT
(The current practice of digital system engineering)
62 W( is not based on science and mathematics. As a result,)63 W
9504 13643 MT
(computer systems in operation today exhibit)
155 W( unforeseen behaviors that cause loss of life, information,)154 W
9504 14929 MT
(property and money.)
17 W( This)
286 W( paper identifies the major scientific and mathematical problems that need to be)18 W
9504 16215 MT
(solved to advance the state of digital system engineering practice.)SH
ES
%%Page: 1 3
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(1)SH
13 /Times-Bold AF
28053 15271 MT
(Chapter 1)SH
25651 17530 MT
(INTRODUCTION)SH
10 /Times-Roman AF
9504 25416 MT
(COMPASS 88. COMPuter ASSurance. Assurance of what?)SH
/Symbol SF
11794 26869 MT
(\267)SH
/Times-Roman SF
12504 XM
("A man with cancer is killed)
236 W( because a computer tells a radiation therapy machine to)235 W
12504 27974 MT
(administer a lethal dose.")SH
/Symbol SF
11794 29732 MT
(\267)SH
/Times-Roman SF
12504 XM
("A rocket on the way to Venus has to be destroyed because)
78 W( a crucial line is left out of the)79 W
12504 30837 MT
(computer software controlling it.")SH
/Symbol SF
11794 32595 MT
(\267)SH
/Times-Roman SF
12504 XM
("A bank is forced to borrow $23.6 billion overnight because of a computer, and)
279 W( the)278 W
12504 33700 MT
(government-securities market narrowly escapes disaster.")SH
/Symbol SF
11794 35458 MT
(\267)SH
/Times-Roman SF
12504 XM
("Workers are killed by computer controlled industrial robots.")SH
9504 38030 MT
(These are quotations from the call for papers for this conference.)
149 W( They)
550 W( get our attention because the)150 W
9504 39316 MT
(behavior of these computer systems caused dramatic loss of life, property)
50 W( and money. What do we want)49 W
9504 40602 MT
(assurance of? We want assurance that computer systems will not cause such harmful effects.)SH
9504 43174 MT
(To gain)
20 W( that assurance, we must eliminate the cause of those effects. What is the common thread that ties)21 W
9504 44460 MT
(these incidents together? What caused these effects? They were caused by a computer system that)190 W
9504 45746 MT
(behaved in some unforeseen way. If any one)
48 W( of these four incidents had been foreseen, would they have)49 W
9504 47032 MT
(been allowed to happen? I certainly hope not.)SH
9504 49604 MT
(These are not isolated incidents. Unforeseen behavior in computer systems is common. In the)319 W
9504 50890 MT
(sophisticated, high-tech vocabulary of our times, we)
15 W( call an instance of unexpected behavior a "bug", or if)16 W
9504 52176 MT
(it's benign, a "feature." If computing bugs were)
132 W( bacteria, someone would surely declare an epidemic.)131 W
9504 53462 MT
(When these instances of unforeseen behavior cause serious effects, we hear about them. Those that do not)4 W
9504 54748 MT
(cause serious effects, we ignore or tolerate as)
65 W( mere inconvenience. But, the ones that are potentially the)64 W
9504 56034 MT
(most dangerous are the ones that we haven't yet discovered.)SH
9504 58606 MT
(The only way to be assured that dangerous bugs do not exist is to peer into the future behavior)
160 W( of a)161 W
9504 59892 MT
(computer system. Past behavior is of no concern. The)
32 W( effects of that behavior already have been caused.)31 W
9504 61178 MT
(We cannot undo them. The only thing we can do anything about is future behavior.)SH
9504 63750 MT
(To get sound assurance that a computer system will)
37 W( not cause harmful effects, we must be able to predict)38 W
9504 65036 MT
(accurately that it)189 W
/Times-Italic SF
16986 XM
(will)SH
/Times-Roman SF
18926 XM
(behave within acceptable limits. Without that predictability, using)
189 W( a computer)188 W
9504 66322 MT
(system is a gamble. The)
3 W( four incidents cited above are ones in which someone gambled, probably without)4 W
9504 67608 MT
(even knowing it, and lost.)SH
ES
%%Page: 2 4
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(2)SH
13 /Times-Bold AF
28053 15271 MT
(Chapter 2)SH
16152 17530 MT
(SCIENCE, MATHEMATICS AND ENGINEERING)SH
10 /Times-Roman AF
9504 25416 MT
(There are four key observations that lead to a rigorous,)
203 W( scientific basis for predicting accurately the)202 W
9504 26702 MT
(behavior of a digital computer system.)SH
9504 29274 MT
(The first observation is that the thing we need to make predictions about is a)
25 W( piece of computer hardware.)26 W
9504 30560 MT
(What we need to predict is)
154 W( the electronic behavior of a small part of the physical universe. It is the)153 W
9504 31846 MT
(electronic behavior of this piece of physical material that causes beneficial or harmful effects in)
197 W( the)198 W
9504 33132 MT
(physical world.)SH
9504 35704 MT
(The second observation)
55 W( is that there are established, well-developed scientific methods for predicting the)54 W
9504 36990 MT
(behavior of the)
201 W( physical world. The most effective way is to identify a mathematical equation that)202 W
9504 38276 MT
(describes the behavior of what we need to predict.)SH
9504 40848 MT
(An example of such an equation is Ohm's Law for metallic conductors,)304 W
/Times-Italic SF
42007 XM
(V=I*R)SH
/Times-Roman SF
(. It describes the)303 W
9504 42134 MT
(mathematical relationship among the)
11 W( voltage, current and resistance of a metallic conductor. A process of)12 W
9504 43420 MT
(current measurement transforms a physical observation about the conductor)
46 W( into a mathematical object, a)45 W
9504 44706 MT
(number. Another)
723 W( process, resistance measurement, transforms a second physical observation into a)237 W
9504 45992 MT
(second number.)
49 W( Then,)
346 W( strictly within the mathematical world, these two numbers are multiplied together)48 W
9504 47278 MT
(to get a third number. By)
75 W( the miracle of mathematics, that third number accurately predicts the number)76 W
9504 48564 MT
(that)SH
/Times-Italic SF
11479 XM
(will be)225 W
/Times-Roman SF
14874 XM
(obtained by measuring the)
225 W( voltage of the conductor. This relationship among physical)224 W
9504 49850 MT
(observation, measurement and mathematics is illustrated in Figure 2-1.)SH
/Times-Bold SF
22992 52598 MT
(Figure 2-1:)SH
/Times-Roman SF
28491 XM
(Science and Mathematics)SH
8 /Courier-Bold AF
21024 55147 MT
(Physical Measurement)
2880 W( Mathematical)3360 W
19104 56092 MT
(Observation <----------------------> Analysis)SH
10 /Times-Roman AF
9504 58840 MT
(The purpose of science is to discover the laws)
SH( of physical behavior. Much of science can be viewed as the)1 W
9504 60126 MT
(search for the mathematical equation that accurately describes some aspect of)
144 W( physical behavior. The)143 W
9504 61412 MT
(mathematical application of those laws to physical systems is the)
2 W( basis of effective engineering. Electrical)3 W
9504 62698 MT
(engineering, for example, is firmly based upon)
150 W( the mathematical application of Ohm's Law and other)149 W
9504 63984 MT
(mathematical equations that accurately describe the physical behavior of electrical circuits.)SH
9504 66556 MT
(The third observation, the one)
31 W( of science, is that there do exist mathematical equations that describe, with)32 W
9504 67842 MT
(a very high degree)
78 W( of accuracy, the physical, electronic behavior of digital computers. The existence of)77 W
9504 69128 MT
(such equations establishes)
158 W( a true scientific relationship between the observable physical behavior of a)159 W
9504 70414 MT
(digital computer and mathematics. Once such equations are)
27 W( identified, the full power of mathematics can)26 W
9504 71700 MT
(be used to analyze the physical behavior of a digital computer.)SH
ES
%%Page: 3 5
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(3)SH
9504 7886 MT
(The final observation, the one of)
44 W( engineering, is that once such equations are identified, they can be used)45 W
9504 9172 MT
(in the practice of engineering to build computing systems with physical behavior that is predictable with a)16 W
9504 10458 MT
(very high degree of accuracy. In fact, one might well wonder how systems with predictable)
30 W( behavior can)31 W
9504 11744 MT
(be engineered without applying them?)SH
ES
%%Page: 4 6
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(4)SH
13 /Times-Bold AF
28053 15271 MT
(Chapter 3)SH
18084 17530 MT
(MATHEMATICS FOR DIGITAL SYSTEMS)SH
10 /Times-Roman AF
9504 25416 MT
(For the sake of concreteness, the presentation in this section is focused on the machine language of a)
16 W( fully)15 W
9504 26702 MT
(synchronous digital system. However,)
29 W( what is said here applies to the behavior of any digital system that)30 W
9504 27988 MT
(can be described accurately by a mathematical equation.)SH
9504 30560 MT
(The key scientific step in predicting the physical behavior of a digital system is)
177 W( to identify the right)176 W
9504 31846 MT
(equation. The)
287 W( equation might define the gate level operation of a digital system, the micro code level, the)19 W
9504 33132 MT
(machine language level, an operating system)
283 W( or a higher level programming language. Thus, the)282 W
9504 34418 MT
(mathematics described here apply both to certain)
115 W( levels of hardware engineering and to all of software)116 W
9504 35704 MT
(engineering. I)
250 W( will refer to all of these levels as "digital system engineering.")SH
9504 38276 MT
(The discussion in this section should be viewed as taking place in the mathematical world shown on)
69 W( the)68 W
9504 39562 MT
(right of Figure 2-1. The identification of the equation that accurately)
28 W( describes the physical behavior of a)29 W
9504 40848 MT
(digital system is what allows us to "cross the measurement)
123 W( bridge" and have mathematical discussions)122 W
9504 42134 MT
(about the behavior of physical systems.)SH
12 /Times-Bold AF
9504 45818 MT
(3.1 Describing)
300 W( System Behavior)SH
10 /Times-Roman AF
9504 48288 MT
(Consider the complete sequence of observable states)
92 W( produced by a fully synchronous digital computer.)93 W
9504 49574 MT
(Include in its state every bit)
66 W( that is observable by a machine language program. This includes the entire)65 W
9504 50860 MT
(address space of the machine)
13 W( \050including its program\051, every observable register and even the system clock)14 W
9504 52146 MT
(\050if it)
119 W( is observable\051. The electronic behavior of such a machine can be described very accurately by a)118 W
9504 53432 MT
(system of equations such as)SH
8 /Courier-Bold AF
11504 54916 MT
(M\050s,t,n\051 =)SH
11984 55861 MT
(if halt\050s\051 or n=0)SH
11984 56806 MT
(then {\050s,t\051})SH
11984 57751 MT
(else {\050s,t\051} @ M\050cycle\050s\051,t+ticks\050s\051,n-1\051)SH
11504 59641 MT
(halt\050s\051 =)
480 W( ...)SH
11504 61531 MT
(cycle\050s\051 = execute\050fetch\050s\051\051)SH
11504 63421 MT
(fetch\050s\051 = ...)SH
11504 65311 MT
(execute\050c\051 = ...)SH
11504 67201 MT
(ticks\050s\051 = ...)SH
10 /Times-Roman AF
9504 69773 MT
(For every)
108 W( triple)109 W
/Times-Italic SF
16301 XM
(\050s0,t0,n\051)SH
/Times-Roman SF
(,)SH
/Times-Italic SF
20243 XM
(M\050s0,t0,n\051)SH
/Times-Roman SF
24768 XM
(produces a sequence of pairs)109 W
/Times-Italic SF
37059 XM
({ \050s0,t0\051, ..., \050sk,tk\051 })109 W
/Times-Roman SF
45958 XM
(where)SH
/Times-Italic SF
48760 XM
(sk)SH
/Times-Roman SF
49952 XM
(is the)109 W
9504 71059 MT
(state of the machine after starting it on state)11 W
/Times-Italic SF
27350 XM
(s0)SH
/Times-Roman SF
28500 XM
(at time)11 W
/Times-Italic SF
31522 XM
(t0)SH
/Times-Roman SF
32561 XM
(and allowing it)
11 W( to run for either)10 W
/Times-Italic SF
45437 XM
(n)SH
/Times-Roman SF
46197 XM
(steps or until it)10 W
ES
%%Page: 5 7
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(5)SH
8 SS
49774 7749 MT
(1)SH
10 SS
9504 8094 MT
(halts. If)
250 W( the machine halts,)SH
/Times-Italic SF
20558 XM
(k<=n)SH
/Times-Roman SF
(; otherwise,)SH
/Times-Italic SF
27768 XM
(k=n)SH
/Times-Roman SF
(. Each)250 W
/Times-Italic SF
32386 XM
(ti)SH
/Times-Roman SF
33192 XM
(is the time at which state)SH
/Times-Italic SF
43358 XM
(si)SH
/Times-Roman SF
44275 XM
(is observable.)SH
9504 10666 MT
(The equations above are defined \050by filling in the ...\051 so that)84 W
/Times-Italic SF
34758 XM
(M\050s,t,n\051)SH
/Times-Roman SF
38258 XM
(defines every component of)
84 W( every)83 W
9504 11952 MT
(state. No)
586 W( steps)
168 W( in the sequence are left out. There are no intermediate states in between successive)169 W
9504 13238 MT
(elements of this sequence.)88 W
/Times-Italic SF
20942 XM
(M\050s,t,n\051)SH
/Times-Roman SF
24446 XM
(defines every observable bit in every observable)
88 W( successive state of)87 W
9504 14524 MT
(the machine and the time at which the state can be observed.)SH
/Times-Bold SF
24561 17272 MT
(Table 3-1:)SH
/Times-Roman SF
29672 XM
(Example Behavior)SH
8 /Courier-Bold AF
25344 19821 MT
(| s0 s1 s2 s3 s4 s5 s6)SH
25344 20766 MT
(----------------------)SH
24864 21711 MT
(1| 1 0 1 0 1 0 0)480 W
24864 22656 MT
(2| 1 0 0 1 0 1 0)480 W
24864 23601 MT
(3| 0 1 0 1 0 0 1)480 W
24864 24546 MT
(4| 0 0 1 0 1 1 0)480 W
24864 25491 MT
(5| 0 0 1 0 1 0 0)480 W
24864 27381 MT
(t| 0 2 3 4 6 8 9)480 W
25344 28326 MT
(----------------------)SH
10 /Times-Roman AF
9504 31074 MT
(To illustrate in more detail, Table 3-1)
70 W( shows what)71 W
/Times-Italic SF
30357 XM
(M\050s0,0,6\051)SH
/Times-Roman SF
34566 XM
(might be if these equations define a simple)71 W
9504 32360 MT
(system with just five state components. The five state components are numbered "1" through "5")
79 W( down)78 W
9504 33646 MT
(the left side of the table. The columns of the table show)
25 W( the values of these components in the successive)26 W
9504 34932 MT
(states "s0" through "s6.")
169 W( The)
586 W( bottom row, labeled "t", is the time of observation of the state in that)168 W
9504 36218 MT
(column. Each)
250 W( column represents one pair)SH
/Times-Italic SF
26556 XM
(\050si,ti\051)SH
/Times-Roman SF
28945 XM
(of the sequence)SH
/Times-Italic SF
35415 XM
({ \050s0,t0\051, ..., \050s6,t6\051 })SH
/Times-Roman SF
(.)SH
11 /Times-Bold AF
9504 39115 MT
(3.1.1 Completeness)275 W
10 /Times-Roman AF
9504 41453 MT
(Any equation that describes accurately some of the components of)
23 W( some of the steps of the state sequence)24 W
9504 42739 MT
(produced by a)
23 W( digital system can be used to predict some aspects of the physical behavior of the machine.)22 W
9504 44025 MT
(For an equation to be useful in predicting that the behavior of a computer)119 W
/Times-Italic SF
40722 XM
(does not cause any)120 W
/Times-Roman SF
49034 XM
(harmful)SH
9504 45311 MT
(effect in its physical environment, the equation also must be)128 W
/Times-Italic SF
35087 XM
(complete)SH
/Times-Roman SF
39075 XM
(in the following)
128 W( sense. It must)127 W
9504 46597 MT
(describe)SH
/Symbol SF
11794 48050 MT
(\267)SH
/Times-Italic SF
12504 XM
(all)SH
/Times-Roman SF
13810 XM
(of the potentially observable state components,)SH
/Symbol SF
11794 49808 MT
(\267)SH
/Times-Italic SF
12504 XM
(all)SH
/Times-Roman SF
13810 XM
(of the potentially observable steps in the state sequence and)SH
/Symbol SF
11794 51566 MT
(\267)SH
/Times-Roman SF
12504 XM
(the)SH
/Times-Italic SF
13976 XM
(time)SH
/Times-Roman SF
15948 XM
(at which each such step occurs.)SH
9504 52905 MT
(If the equation does not describe all of these things, it)
108 W( is easy to imagine how harmful physical effects)109 W
9504 54191 MT
(could be caused by some system behavior that was outside)
12 W( the scope of the equation. If just one single bit)11 W
9504 55477 MT
(falls outside the scope of the equation, it could be the one)
57 W( that sends the wrong electrical signal or sends)58 W
9504 56763 MT
(the right signal at the wrong time.)SH
9504 59335 MT
(At this point, I'd like to state an opinion about)
41 W( the use of partial recursive functions to describe computer)40 W
9504 60621 MT
(behavior. Traditionally,)
448 W( partial recursive functions have been used to describe the relationship)
99 W( between)100 W
9504 61907 MT
(the initial and final state of a machine. Such a description accurately describes some aspects of)
182 W( the)181 W
9504 63193 MT
(behavior of the)
194 W( physical system, but it is not complete because it may not describe the sequence of)195 W
9504 64479 MT
(intermediate observable states. An incomplete description is not)
247 W( sufficient to show the absence of)246 W
9504 65765 MT
(behaviors that cause harmful effects. \050I doubt that the family of the person who)
221 W( died from excess)222 W
9504 67051 MT
(radiation would have taken much comfort from the fact that when the)
249 W( program that controlled the)248 W
10800 50 9504 69428 UL
6 SS
10304 70767 MT
(1)SH
8 SS
10604 71076 MT
(We assume that the)25 W
/Times-Italic SF
17144 XM
(ti)SH
/Times-Roman SF
17813 XM
(are monotonically increasing. This is a realistic assumption about a physical system,)
25 W( and it ensures that)26 W
/Times-Italic SF
51622 XM
(m)SH
/Times-Roman SF
9504 72000 MT
(is a function -- i.e, it maps every triple into a unique sequence.)SH
ES
%%Page: 6 8
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(6)SH
9504 7886 MT
(radiation device stopped, it shut off the radiation source.\051 Also, the traditional use of partial)
122 W( recursive)123 W
9504 9172 MT
(functions has omitted timing issues. Intermediate system states and)
180 W( timing are important, sometimes)179 W
9504 10458 MT
(critical, aspects of the behavior of a physical system. Effective engineering cannot ignore them.)SH
9504 13030 MT
(This is not to say that we should avoid using partial recursive functions to describe the)
46 W( physical behavior)47 W
9504 14316 MT
(of digital systems.)
7 W( We)
263 W( should use whatever mathematics accurately describes the physical behavior of the)6 W
9504 15602 MT
(system. I)
298 W( suspect, however, that the mathematical)
24 W( emphasis on partial recursive functions that map initial)25 W
9504 16888 MT
(states into final states)
15 W( and on their termination has distracted us from some of the important things that we)14 W
9504 18174 MT
(need to)
59 W( describe about physical systems -- namely, intermediate states and timing. Certainly, sometimes)60 W
9504 19460 MT
(we do want to)
37 W( know that a computer will stop running. But sometimes, particularly when it's controlling)36 W
9504 20746 MT
(a physical device, we want to know that it does)49 W
/Times-Italic SF
29130 XM
(not)SH
/Times-Roman SF
30707 XM
(stop; and we want to know what)
49 W( it's doing while it's)50 W
9504 22032 MT
(running and how fast it's doing it.)SH
11 /Times-Bold AF
9504 24929 MT
(3.1.2 Magnitude)275 W
10 /Times-Roman AF
9504 27267 MT
(The matrix in Table 3-1 makes)
227 W( clear some of the massive complexity that confronts digital system)226 W
9504 28553 MT
(engineering. Suppose)
388 W( we ignore)
69 W( timing and consider just the progression of the system state through its)70 W
9504 29839 MT
(successive transitions. Each such behavior of a system is represented accurately by)
32 W( one value of a matrix)31 W
9504 31125 MT
(like the one in Table 3-1. How many such behaviors are there?)SH
9504 33697 MT
(The matrix gives us a clear way to count them.)
29 W( For)
310 W( a binary computer system, there are just two possible)30 W
9504 34983 MT
(values for each position in the matrix. Thus, the matrix has)SH
12004 36503 MT
(2^\050m*n\051)SH
51034 XM
(\0501\051)SH
9504 38023 MT
(possible values where)65 W
/Times-Italic SF
18725 XM
(m)SH
/Times-Roman SF
19762 XM
(is its number of rows and)65 W
/Times-Italic SF
30540 XM
(n)SH
/Times-Roman SF
31355 XM
(is its number of columns. Just the trivial matrix in)65 W
9504 39309 MT
(Table 3-1 has)20 W
/Times-Italic SF
15257 XM
(2^35)SH
/Times-Roman SF
17449 XM
(possible values. Those two innocent looking numbers give more)
20 W( than 34 * 10^9, over)21 W
9504 40595 MT
(34 billion possible behaviors for one absolutely trivial system.)SH
9504 43167 MT
(For a real computer system, what are)12 W
/Times-Italic SF
24640 XM
(m)SH
/Times-Roman SF
25624 XM
(and)SH
/Times-Italic SF
27330 XM
(n)SH
/Times-Roman SF
(? The number)12 W
/Times-Italic SF
33669 XM
(m)SH
/Times-Roman SF
34652 XM
(is the total number of observable single bits)11 W
9504 44453 MT
(in a system, and)117 W
/Times-Italic SF
16666 XM
(n)SH
/Times-Roman SF
17533 XM
(is the)
117 W( total number of observable state transitions the computer makes over a given)118 W
9504 45739 MT
(period of time. For modern computer systems, these numbers themselves are huge.)
71 W( How)
390 W( many bits are)70 W
9504 47025 MT
(there in a 32-bit address space of 32 bit words?)
17 W( 2^37.)
285 W( This is over 137 * 10^9. If a computer makes state)18 W
9504 48311 MT
(transitions a rate of one every 100 nano-seconds, how many does it make in just one)
67 W( minute?)66 W
/Times-Italic SF
48396 XM
(6 * 10^8)66 W
/Times-Roman SF
(.)SH
9504 49597 MT
(How many different ways might such a machine behave in just)
53 W( one minute? More than 2 ^ \0508 * 10^19\051.)54 W
9504 50883 MT
(Think about that number. You can't. It's just too big.)
33 W( But)
315 W( is there any doubt that just one bit in just one)32 W
9504 52169 MT
(state of just one of those behaviors could cause a harmful effect in the physical world? No. And, what)
13 W( are)14 W
9504 53455 MT
(hardware manufacturers doing for us? Building bigger and faster computers)149 W
/Times-Italic SF
41997 XM
(and)SH
/Times-Roman SF
43895 XM
(making them run in)148 W
9504 54741 MT
(parallel!)SH
11 /Times-Bold AF
9504 57638 MT
(3.1.3 Instability)275 W
10 /Times-Roman AF
9504 59976 MT
(Another major complexity that confronts the digital)
79 W( system engineer is the instability of digital systems.)80 W
9504 61262 MT
(Just as a single bit in a single state can)
49 W( cause a harmful effect in the physical world, it also can cause the)48 W
9504 62548 MT
(behavior of a digital system to progress in radically different ways.)SH
9504 65120 MT
(If digital systems were)
17 W( stable, a small change in)18 W
/Times-Italic SF
29049 XM
(s)SH
/Times-Roman SF
29706 XM
(would yield a small change in)18 W
/Times-Italic SF
42035 XM
(M\050s,t,n\051)SH
/Times-Roman SF
(. Digital)
286 W( systems)18 W
9504 66406 MT
(are about as far from being stable as one can imagine. The tiniest)
18 W( possible change in)17 W
/Times-Italic SF
43966 XM
(s)SH
/Times-Roman SF
(, one single bit, can)17 W
9504 67692 MT
(yield radically different results in)88 W
/Times-Italic SF
23525 XM
(M\050s,t,n\051)SH
/Times-Roman SF
(. There)
426 W( is no continuity in)89 W
/Times-Italic SF
38145 XM
(M\050s,t,n\051)SH
/Times-Roman SF
(. Computer)
428 W( programs in)89 W
/Times-Italic SF
51811 XM
(s)SH
/Times-Roman SF
9504 68978 MT
(must be expressed accurately to mega-bits of precision. Continuity is what many)
207 W( other engineering)206 W
9504 70264 MT
(disciplines use to build)
129 W( safety factors into their systems. This safety net is not available to the digital)130 W
9504 71550 MT
(system engineer.)SH
ES
%%Page: 7 9
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(7)SH
12 /Times-Bold AF
9504 8004 MT
(3.2 Defining)
300 W( Acceptable Behavior)SH
10 /Times-Roman AF
9504 10474 MT
(Once we have a mathematical equation)
95 W( that describes the physical behavior of a digital system, the full)94 W
9504 11760 MT
(power of mathematics becomes available for us to use to manage this complexity. One)
198 W( of the first)199 W
9504 13046 MT
(important things that becomes available to us is the ability to state a rigorous,)
56 W( mathematical definition of)55 W
/Times-Italic SF
9504 14332 MT
(acceptable)SH
/Times-Roman SF
14178 XM
(system behavior. We can state an acceptance test that distinguishes between)
92 W( acceptable and)93 W
9504 15618 MT
(unacceptable behavior.)SH
9504 18190 MT
(Suppose that)
19 W( we have a function, such as)18 W
/Times-Italic SF
26285 XM
(M\050s,t,n\051)SH
/Times-Roman SF
29719 XM
(above, that accurately describes system behavior. Once)18 W
/Times-Italic SF
9504 19476 MT
(M\050s,t,n\051)SH
/Times-Roman SF
12938 XM
(is identified, we can choose an acceptance test)
18 W( function)19 W
/Times-Italic SF
35485 XM
(A)SH
/Times-Roman SF
36365 XM
(that maps every system behavior into)19 W
/Times-Italic SF
51644 XM
(T)SH
/Times-Roman SF
9504 20762 MT
(if the behavior)SH
/Times-Italic SF
15586 XM
(M\050s,t,n\051)SH
/Times-Roman SF
19002 XM
(is "acceptable" and into)SH
/Times-Italic SF
28705 XM
(F)SH
/Times-Roman SF
29566 XM
(if it is "unacceptable.")SH
9504 23334 MT
(For predictability, it is important that the acceptance test be conclusive. That is,)
202 W( for every possible)201 W
9504 24620 MT
(behavior, the test must tell us, "Yes, this behavior is acceptable")
19 W( or "No, it is not." There is no room for a)20 W
9504 25906 MT
(middle ground. To make a conclusive prediction, one must have a conclusive test. Therefore,)
235 W( an)234 W
9504 27192 MT
(acceptance test must be chosen so that it produces with)SH
/Times-Italic SF
31778 XM
(T)SH
/Times-Roman SF
32584 XM
(or)SH
/Times-Italic SF
33667 XM
(F)SH
/Times-Roman SF
34528 XM
(for every possible behavior.)SH
9504 29764 MT
(The full power)
9 W( of mathematics can be used to state an acceptance test. The test)10 W
/Times-Italic SF
41682 XM
(may)SH
/Times-Roman SF
43608 XM
(contain mathematical)10 W
9504 31050 MT
(objects and functions that do not have physical counterparts. For example, the acceptance test)
51 W( might use)50 W
9504 32336 MT
(functions on real or imaginary numbers. The only practical requirement for predictability is that the test)63 W
8 SS
32444 33277 MT
(2)SH
10 SS
9504 33622 MT
(produce either)SH
/Times-Italic SF
15502 XM
(T)SH
/Times-Roman SF
16308 XM
(or)SH
/Times-Italic SF
17391 XM
(F)SH
/Times-Roman SF
18252 XM
(for every possible system behavior.)SH
9504 36194 MT
(Discovering a good acceptance test)
122 W( for various purposes may be difficult. In searching for acceptance)121 W
9504 37480 MT
(tests that will demonstrate that a system has no behavior that causes a harmful)
211 W( effect, one must be)212 W
9504 38766 MT
(especially careful. First, one must begin with a complete description of the)
47 W( system, so that one is certain)46 W
9504 40052 MT
(that all possible behaviors are described. Then, one must find an)
59 W( acceptance test that definitely does not)60 W
9504 41338 MT
(accept)SH
/Times-Italic SF
12309 XM
(any)SH
/Times-Roman SF
14004 XM
(harmful behavior. A test that rejects all)
1 W( harmful behaviors along with some others is sufficient,)SH
9504 42624 MT
(but it)SH
/Times-Italic SF
11838 XM
(must)SH
/Times-Roman SF
13977 XM
(reject)SH
/Times-Italic SF
16448 XM
(every one)SH
/Times-Roman SF
20557 XM
(of the harmful ones.)SH
9504 45196 MT
(Once an acceptance test is chosen,)SH
/Times-Italic SF
11504 46716 MT
(A\050M\050s,t,n\051\051 = T)SH
/Times-Roman SF
17928 XM
(for all behaviors)SH
51034 XM
(\0502\051)SH
9504 48236 MT
(is a rigorous mathematical statement of acceptable system)
92 W( behavior. If this equation is true, then every)93 W
9504 49522 MT
(behavior described by)79 W
/Times-Italic SF
18822 XM
(M\050s,t,n\051)SH
/Times-Roman SF
22317 XM
(is acceptable. Every possible behavior)
79 W( passes the acceptance test. None)78 W
9504 50808 MT
(fail. The)
736 W( system has no unforeseen, unacceptable behavior. Equation 2)
243 W( is a precise mathematical)244 W
9504 52094 MT
(statement of "This system will behave acceptably.")SH
9504 54666 MT
(I emphasize that the acceptance test is defined mathematically. It is a mathematical function. It is not)
59 W( a)58 W
9504 55952 MT
(physical test. This is done quite purposefully for)
257 W( two reasons. The first is that it enables all of)258 W
9504 57238 MT
(mathematics to be used in expressing acceptance tests. The second reason is)
7 W( that it avoids the necessity of)6 W
9504 58524 MT
(physical measurements and the serious physical problems that may be associated with making them.)SH
9504 61096 MT
(The first problem is that one must have a)
74 W( physical system to measure. With the acceptance test defined)75 W
9504 62382 MT
(strictly mathematically, one can rigorously analyze the behavior of a)
36 W( digital system)35 W
/Times-Italic SF
43456 XM
(before)SH
/Times-Roman SF
46296 XM
(it is physically)35 W
9504 63668 MT
(constructed. This)
290 W( enables an engineer to evaluate alternative system structures objectively before)
20 W( actually)21 W
10800 50 9504 66656 UL
6 SS
10304 67995 MT
(2)SH
8 SS
10604 68304 MT
(These considerations have implications for formal specification languages. A specification language should)
42 W( provide a means of)41 W
9504 69228 MT
(stating i\051 the equations that describe system behavior and ii\051 acceptance tests. For predictability,)
16 W( the language should require that all)17 W
9504 70152 MT
(acceptance tests be conclusive, -- i.e., produce either)209 W
/Times-Italic SF
28184 XM
(T)SH
/Times-Roman SF
29037 XM
(or)SH
/Times-Italic SF
30111 XM
(F)SH
/Times-Roman SF
(. Most)
616 W( current specification languages provide only a part of)208 W
9504 71076 MT
(mathematics. Therefore,)
264 W( they limit the acceptance tests that can be stated. A notable exception is Z)
33 W( [Hayes)
SH( 87] which is a notation)33 W
9504 72000 MT
(based on elementary set theory.)SH
ES
%%Page: 8 10
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(8)SH
9504 7886 MT
(building them. This has strong economic implications in both hardware and software engineering.)SH
9504 10458 MT
(A second problem is)
91 W( that physical measurement must measure the right thing. One must know that the)90 W
9504 11744 MT
(measurement instrument is making the right transformation from physical)
76 W( phenomena into mathematical)77 W
9504 13030 MT
(objects. This,)
556 W( too, has strong implications)
153 W( for both hardware and software engineering. Measuring a)152 W
9504 14316 MT
(machine state is not a simple task.)SH
9504 16888 MT
(A third problem is that sometimes measurement perturbs the physical phenomena being)
2 W( measured. This is)3 W
9504 18174 MT
(an important issue for acceptance tests that involve timing.)
32 W( How)
312 W( can one be sure that the instrumentation)31 W
9504 19460 MT
(that measures the timing has no effect on timing?)SH
9504 22032 MT
(A fourth problem is the repeatability)
217 W( of system behavior. A physical experiment is of no value in)218 W
9504 23318 MT
(predicting future behavior unless the behavior is)
88 W( repeatable in time. For a physical measurement of the)87 W
9504 24604 MT
(acceptance test to be useful as a predictor, there must be some)
407 W( amount of time)408 W
/Times-Italic SF
47051 XM
(u)SH
/Times-Roman SF
48209 XM
(such that)408 W
/Times-Italic SF
9504 25890 MT
(A\050M\050s,t,n\051\051 = A\050M\050s,t+u,n\051\051)56 W
/Times-Roman SF
21157 XM
(where)SH
/Times-Italic SF
23905 XM
(u)SH
/Times-Roman SF
24710 XM
(is enough time to make and evaluate the physical measurement and)55 W
9504 27176 MT
(to restart the system. There are a great many systems for which this is not true.)SH
12 /Times-Bold AF
9504 30860 MT
(3.3 Demonstrating)
300 W( Acceptable Behavior)SH
10 /Times-Roman AF
9504 33330 MT
(Equation 2 is the mathematical statement of acceptable system behavior. Given this)
259 W( mathematical)260 W
9504 34616 MT
(formulation, the full power of mathematical analysis can be used to demonstrate that this equation is true.)SH
11 /Times-Bold AF
9504 37513 MT
(3.3.1 Enumeration)275 W
10 /Times-Roman AF
9504 39851 MT
(Normally, one would not begin a discussion about proving a mathematical)
80 W( equation by discussing proof)79 W
9504 41137 MT
(by enumeration. But that's what I'm going to do. The reason for this is that what is said in this)
62 W( section)63 W
9504 42423 MT
(also applies to)
154 W( the physical testing of systems, and physical testing is the current state of engineering)153 W
9504 43709 MT
(practice.)SH
9504 46281 MT
(In principle, one can prove Equation 2 by evaluating it for all possible cases)
119 W( of system behavior. The)120 W
9504 47567 MT
(practical problem with this is the overwhelming number)
151 W( of cases of possible system behavior, as was)150 W
9504 48853 MT
(illustrated earlier.)SH
9504 51425 MT
(As another example, suppose we were going to)
51 W( demonstrate the truth of Equation 2 for a 32 bit adder by)52 W
9504 52711 MT
(physically testing its addition of all possible pairs of)
21 W( 32 bit numbers. This would require 2^64 \050more than)20 W
9504 53997 MT
(1.84*10^19\051 additions. At a rate of, say)
103 W( 100 nano-seconds per test, this would take over 58,000 years.)104 W
9504 55283 MT
(The adder won't last that long, and neither will the)
17 W( person waiting for the results! One might also wonder)16 W
9504 56569 MT
(how those results are going to be checked and how long that might take?)
50 W( What)
352 W( then, of testing a system)51 W
9504 57855 MT
(with more than a 64-bit state?)SH
9504 60427 MT
(These calculations about the number of possible system behaviors tell us)
78 W( something important about the)77 W
9504 61713 MT
(effectiveness of using enumeration to prove)
111 W( Equation 2. Enumeration can be effective)112 W
/Times-Italic SF
45836 XM
(only if)112 W
/Times-Roman SF
48838 XM
(the total)112 W
8 SS
29180 62654 MT
(3)SH
10 SS
9504 62999 MT
(number of possible system behaviors is small.)210 W
30040 XM
(If the number)
210 W( is not small, some kind of additional)209 W
9504 64285 MT
(mathematical analysis is)
149 W( required in addition to, or instead of, enumeration. We can be more precise)150 W
9504 65571 MT
(about this, as follows.)SH
10800 50 9504 68504 UL
6 SS
10304 69843 MT
(3)SH
8 SS
10604 70152 MT
(Strictly speaking, Dijkstra's often quoted comment "Program testing can be used to show the presence of bugs,)
7 W( but never to show)6 W
9504 71076 MT
(their absence")
46 W( [Dahl)
SH( 72] is not true. The statement was made in the context of an adder example similar to the one given)
46 W( here. In)47 W
9504 72000 MT
(that context, it is quite true.)SH
ES
%%Page: 9 11
BS
0 SI
10 /Times-Roman AF
51700 4286 MT
(9)SH
9504 7886 MT
(Suppose we select)
118 W( some set of behaviors and use them as a "test pattern" by evaluating Equation 2 on)117 W
9504 9172 MT
(them, and)
126 W( suppose that the results of those evaluations tell us whether the equation is true or false for)127 W
9504 10458 MT
(some specific number of)
73 W( behaviors)72 W
/Times-Italic SF
24114 XM
(k)SH
/Times-Roman SF
(. A)
394 W( measure of the effectiveness of this test pattern is)72 W
/Times-Italic SF
47112 XM
(k)SH
/Times-Roman SF
47878 XM
(divided by)72 W
9504 11744 MT
(the total number of possible system behaviors. If we ignore timing, the effectiveness of a test pattern is)SH
12004 13264 MT
(k / 2^\050m*n\051)SH
51034 XM
(\0503\051)SH
9504 14784 MT
(where)SH
/Times-Italic SF
12501 XM
(m)SH
/Times-Roman SF
13777 XM
(is the number of observable state components and)304 W
/Times-Italic SF
36428 XM
(n)SH
/Times-Roman SF
37483 XM
(is the number of observable state)305 W
8 SS
13921 15725 MT
(4)SH
10 SS
9504 16070 MT
(transitions.)SH
9504 18642 MT
(If we choose a test pattern of)48 W
/Times-Italic SF
21642 XM
(k)SH
/Times-Roman SF
22384 XM
(distinct behaviors, and)
48 W( all it tells us is the value of Equation 2 for those)47 W
/Times-Italic SF
51756 XM
(k)SH
/Times-Roman SF
9504 19928 MT
(behaviors, then Equation 3 shows the basic futility of)
52 W( proof by enumeration as a means of demonstrating)53 W
9504 21214 MT
(the truth of Equation 2. The numerator increases only linearly with the size of)
103 W( the test pattern, but the)102 W
9504 22500 MT
(denominator increases exponentially with the product of the number of observable state)
9 W( components times)10 W
9504 23786 MT
(the number of observable state transitions. In most practical situations, the effectiveness measure has)
71 W( to)70 W
9504 25072 MT
(be incredibly small; proof by enumeration is just not effective.)SH
9504 27644 MT
(Equation 3 also shows what is necessary)
33 W( to achieve effective proof by enumeration. Essentially, we have)34 W
9504 28930 MT
(two choices; increase the numerator or decrease the denominator.)SH
9504 31502 MT
(To increase the numerator, we must have a)
212 W( test pattern of)211 W
/Times-Italic SF
34993 XM
(k)SH
/Times-Roman SF
35898 XM
(behaviors that determines the value of)211 W
9504 32788 MT
(Equation 2 for many more than)92 W
/Times-Italic SF
22832 XM
(k)SH
/Times-Roman SF
23618 XM
(behaviors. That)
435 W( only can be done in the presence of some additional)93 W
9504 34074 MT
(kind of)
20 W( mathematical analysis of Equation 2. For proof by enumeration to be effective \050in the presence of)19 W
9504 35360 MT
(a large denominator in Equation 3\051, it)274 W
/Times-Italic SF
26698 XM
(must)SH
/Times-Roman SF
29112 XM
(be done in conjunction with some additional kind of)275 W
9504 36646 MT
(mathematical analysis.)SH
9504 39218 MT
(There are instances of "powerful" test patterns in mathematics. For example, given the proof)
198 W( of an)197 W
9504 40504 MT
(induction hypothesis,)46 W
/Times-Italic SF
18402 XM
(H\050n\051->H\050n+1\051)SH
/Times-Roman SF
(, the test pattern 0 is 100% effective for)
46 W( proving that)47 W
/Times-Italic SF
46033 XM
(H\050n\051)SH
/Times-Roman SF
48218 XM
(is true for)47 W
9504 41790 MT
(all)SH
/Times-Italic SF
10779 XM
(n>=0)SH
/Times-Roman SF
(. As)
300 W( another)
25 W( example, for a polynomial)24 W
/Times-Italic SF
29488 XM
(p\050x\051)SH
/Times-Roman SF
31372 XM
(of degree)24 W
/Times-Italic SF
35418 XM
(k)SH
/Times-Roman SF
(, a test pattern of any)24 W
/Times-Italic SF
44643 XM
(k+1)SH
/Times-Roman SF
46536 XM
(distinct points)24 W
9504 43076 MT
(is 100% effective. Such examples give some hope of the viability of using mathematical)
160 W( analysis of)161 W
9504 44362 MT
(Equation 2 to identify effective test patterns.)SH
9504 46934 MT
(Now, let's consider the denominator)
155 W( of the effectiveness measure. The only way we can get a small)154 W
9504 48220 MT
(denominator is with a small)32 W
/Times-Italic SF
21025 XM
(m*n)SH
/Times-Roman SF
(. There)
314 W( are two ways to do this.)
32 W( Either)
315 W( the acceptance test must involve)33 W
9504 49506 MT
(only a small number of state components and a small number of state)
16 W( transitions, or the system itself must)15 W
9504 50792 MT
(have only a small number of states and transitions.)SH
9504 53364 MT
(One very important instance of this is the functional behavior of low level hardware components.)
56 W( These)364 W
9504 54650 MT
(are digital systems for which physical testing can be effective. One of the challenges of)
223 W( hardware)222 W
9504 55936 MT
(engineering is to design systems so that small)
236 W( components and their interconnections can be tested)237 W
9504 57222 MT
(individually, and also so that mathematical analysis can be used subsequently to deduce that)
310 W( the)309 W
9504 58508 MT
(interconnected hardware satisfies a more)
167 W( complex mathematical equation \050that cannot be exhaustively)168 W
9504 59794 MT
(tested\051.)SH
9504 62366 MT
(Finally, we should note that analysis of the physical environment in which)
35 W( a system operates also may be)34 W
9504 63652 MT
(effective in reducing the)
104 W( total number of behaviors that need to be considered. The observations made)105 W
9504 64938 MT
(above about)
15 W( numbers of behaviors tell us that, during its useful life time, a digital system will exhibit only)14 W
9504 66224 MT
(a very tiny fraction of its total possible number of behaviors. If, somehow, we can isolate those particular)19 W
9504 67510 MT
(behaviors, we may be able to increase the practical effectiveness of proof by enumeration.)SH
10800 50 9504 70352 UL
6 SS
10304 71691 MT
(4)SH
8 SS
10604 72000 MT
(A test that is 100% effective is an "ideal test" in the sense of [Goodenough & Gerhart 75].)SH
ES
%%Page: 10 12
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(10)SH
11 /Times-Bold AF
9504 7937 MT
(3.3.2 Probabilistic)
275 W( Analysis)SH
10 /Times-Roman AF
9504 10275 MT
(Another mathematical technique that)
35 W( should not be overlooked is probabilistic analysis. Ideally, we want)34 W
9504 11561 MT
(Equation 2 to be true for all)
46 W( possible system behaviors. However, for some systems, it may be sufficient)47 W
9504 12847 MT
(to show that the probability of Equation 2 being true on any given behavior is sufficiently high.)285 W
9504 14133 MT
(Conversely, it may be sufficient to show that the probability)
150 W( of some particularly harmful behavior is)151 W
9504 15419 MT
(sufficiently low. Or, we might use probabilistic analysis in conjunction with other analysis. We might)94 W
9504 16705 MT
(show that the probability of good behavior is high and prove that)
57 W( there are no harmful behaviors. All of)58 W
9504 17991 MT
(these are plausible, mathematically)
119 W( rigorous approaches to gaining assurance that a system will behave)118 W
9504 19277 MT
(within acceptable limits.)SH
11 /Times-Bold AF
9504 22174 MT
(3.3.3 Deduction)275 W
10 /Times-Roman AF
9504 24512 MT
(Once we)
12 W( have a function, such as)13 W
/Times-Italic SF
23201 XM
(M\050s,t,n\051)SH
/Times-Roman SF
(, that describes the physical behavior of a digital system, we can)13 W
9504 25798 MT
(apply the full power of mathematical deduction to analyze the behavior of the physical system.)
71 W( We)
390 W( can)70 W
9504 27084 MT
(use the techniques described above or many others.)SH
9504 29656 MT
(There is one deductive approach that may be particularly effective)
93 W( in showing the absence of behaviors)94 W
9504 30942 MT
(that cause harmful effects. It is based on the idea of "hazard analysis" [Leveson 86].)SH
9504 33514 MT
(Suppose that a computer system has the potential to)
6 W( cause some particularly hazardous effect. We want to)5 W
9504 34800 MT
(show that not)
35 W( one single behavior causes this effect. To start, we must begin with a complete description)36 W
9504 36086 MT
(of the)
112 W( physical behavior of the system,)111 W
/Times-Italic SF
26002 XM
(M\050s,t,n\051)SH
/Times-Roman SF
(. Then,)
472 W( instead of an "acceptance" test, let's think of a)111 W
9504 37372 MT
("hazard" test)
12 W( and identify a function)13 W
/Times-Italic SF
24283 XM
(Hazard\050M\050s,t,n\051\051)SH
/Times-Roman SF
31378 XM
(that produces)13 W
/Times-Italic SF
37014 XM
(T)SH
/Times-Roman SF
37833 XM
(for every possible behavior that can)13 W
9504 38658 MT
(cause the hazardous effect.)SH
9504 41230 MT
(Given the complete system description and the hazard test,)
119 W( attempt to prove that the system)118 W
/Times-Italic SF
48111 XM
(does)SH
/Times-Roman SF
50312 XM
(have)SH
9504 42516 MT
(some behavior that satisfies)
162 W( the hazard test. Try to prove that there exists some)163 W
/Times-Italic SF
43941 XM
(s, t)163 W
/Times-Roman SF
45684 XM
(and)SH
/Times-Italic SF
47541 XM
(n)SH
/Times-Roman SF
48454 XM
(such that)163 W
/Times-Italic SF
9504 43802 MT
(Hazard\050M\050s,t,n\051\051=T)SH
/Times-Roman SF
(. The)
400 W( attainment of a logical contradiction proves that no)
75 W( such behaviors exist. If a)74 W
9504 45088 MT
(proof is obtained constructively, it will exhibit)SH
/Times-Italic SF
28337 XM
(some)SH
/Times-Roman SF
30642 XM
(of the hazardous behaviors.)SH
9504 47660 MT
(Finally, let me close this section by returning)
74 W( to the issue of timing. In some applications, timing is the)75 W
9504 48946 MT
(critical requirement of system behavior.)
21 W( I)
291 W( have mentioned the difficulties of physically instrumenting and)20 W
9504 50232 MT
(testing a system for time dependent behavior. For acceptance tests that involve time, there is little)
8 W( hope of)9 W
9504 51518 MT
(proving Equation 2 by enumeration. Thus, it seems that mathematical analysis is the)
79 W( only real hope we)78 W
9504 52804 MT
(have for making accurate predictions about real-time behavior.)SH
9504 55376 MT
(This position actually is supported by current engineering practice.)
229 W( When)
710 W( real-time performance is)230 W
9504 56662 MT
(critical, system builders typically resort to assembly language \050or lower\051 so they can)
73 W( get accurate timing)72 W
9504 57948 MT
(information. Then,)
586 W( they add up instruction times or bounds on)
168 W( instruction times. This is simple \050or)169 W
9504 59234 MT
(maybe not so simple\051 mathematical analysis.)SH
12 /Times-Bold AF
9504 62918 MT
(3.4 Scaling)
300 W( Up)SH
10 /Times-Roman AF
9504 65388 MT
(Many who have read this far may be thinking that it is just not possible to deal)
99 W( with the equations that)98 W
9504 66674 MT
(mathematically describe the physical behavior of a computer system.)
36 W( They)
324 W( are just too complex. I agree)37 W
9504 67960 MT
(that they)
68 W( are complex, but my answer is that we have no alternative but to deal with them and deal with)67 W
9504 69246 MT
(them mathematically. Those are the)
SH( equations that)1 W
/Times-Italic SF
30143 XM
(do)SH
/Times-Roman SF
31394 XM
(describe, very accurately, the physical behavior of a)1 W
9504 70532 MT
(digital computer. The equations do not increase the complexity of the computer system. They)
61 W( reveal it.)60 W
9504 71818 MT
(It is not the complexity of mathematics that confronts us; it)
21 W( is the complexity of computing. Mathematics)22 W
ES
%%Page: 11 13
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(11)SH
9504 7886 MT
(is the best tool we have to master it.)SH
11 /Times-Bold AF
9504 10783 MT
(3.4.1 Equations)
275 W( for Scaling)SH
10 /Times-Roman AF
9504 13121 MT
(One of the main aspects of the complexity that confronts us is)
187 W( the sheer number of possible system)186 W
9504 14407 MT
(behaviors. The)
344 W( structure)
47 W( of Table 3-1 and Equation 1 provide some valuable insight into how to manage)48 W
9504 15693 MT
(this aspect of complexity. We need to reduce the number of rows and columns of the matrix.)SH
9504 18265 MT
(The number of rows in the matrix is determined by)
179 W( the number of observable state transitions. The)178 W
9504 19551 MT
(number of columns is the number of observable state components.)
139 W( To)
529 W( reduce the number of possible)140 W
9504 20837 MT
(behaviors we have two choices; to reduce the number of rows or reduce the)
112 W( number of columns. And)111 W
9504 22123 MT
(surely, we have to do both. But to know that a computer does not cause certain)
28 W( physical effects, we must)29 W
9504 23409 MT
(be able to make a statement about every one of those state components and transitions, and those)
110 W( state)109 W
9504 24695 MT
(components and transitions are real, physical things. Every row of that matrix describes a real, physical)70 W
9504 25981 MT
(object, composed of atomic matter. Every column describes an event in)
41 W( real time. How can we possibly)40 W
9504 27267 MT
(reduce the size of this matrix?)SH
9504 29839 MT
(The answer is to control what can)
26 W( be)27 W
/Times-Italic SF
24655 XM
(observed)SH
/Times-Roman SF
28542 XM
(about this real, physical object. We limit the observability)27 W
8 SS
27306 30780 MT
(5)SH
10 SS
9504 31125 MT
(of various rows and columns in the matrix.)91 W
28388 XM
(This, however, must be done very carefully. We must be)90 W
9504 32411 MT
(absolutely certain that the ability to observe the digital system is limited in exactly the way we think it is.)SH
9504 34983 MT
(We cannot)136 W
/Times-Italic SF
14330 XM
(change)SH
/Times-Roman SF
17604 XM
(the behavior of a physical digital system. But by controlling the way in)
136 W( which its)137 W
9504 36269 MT
(physical behavior can be observed, we can)
47 W( create an illusion about its behavior. This illusion can reduce)46 W
9504 37555 MT
(the observable number of possible system behaviors.)SH
/Times-Bold SF
25088 40303 MT
(Figure 3-1:)SH
/Times-Roman SF
30587 XM
(Virtual System)SH
8 /Courier-Bold AF
30144 42852 MT
(M2)SH
27264 43797 MT
(o----------->o)SH
27264 44742 MT
(| ^)5280 W
27264 45687 MT
(| |)5280 W
22464 46632 MT
(decompose |)
SH( |)
5280 W( compose)SH
27264 47577 MT
(| |)5280 W
27264 48522 MT
(v |)5280 W
27264 49467 MT
(o----------->o)SH
29664 50412 MT
(M1)SH
10 /Times-Roman AF
9504 53160 MT
(One way to do this is with a scaling equation such as)SH
8 /Times-Italic AF
11504 54652 MT
(M2[s,t,n] = compose\050s, M1[decompose\050s,t\051,t,steps\050s,t,n\051], t, n\051)SH
/Courier-Bold SF
50760 XM
(\0504\051)SH
11504 56542 MT
(provided)SH
/Times-Italic SF
15824 XM
(ready\050s,decompose\050s,t\051,t\051)SH
10 /Times-Roman AF
9504 58173 MT
(This equation describes a)175 W
/Times-Italic SF
20591 XM
(virtual)SH
/Times-Roman SF
23683 XM
(system)SH
/Times-Italic SF
26887 XM
(M2)SH
/Times-Roman SF
28646 XM
(that is created by limiting the observation of a physical)176 W
9504 59459 MT
(system)SH
/Times-Italic SF
12640 XM
(M1)SH
/Times-Roman SF
(. The)
466 W( function)108 W
/Times-Italic SF
20543 XM
(steps)SH
/Times-Roman SF
22901 XM
(controls observation of the state transitions, and)
108 W( the functions)107 W
/Times-Italic SF
48701 XM
(compose)SH
/Times-Roman SF
9504 60745 MT
(and)SH
/Times-Italic SF
11258 XM
(decompose)SH
/Times-Roman SF
16011 XM
(control observation of the state components. The relation)60 W
/Times-Italic SF
39881 XM
(ready)SH
/Times-Roman SF
42468 XM
(describes the conditions)61 W
9504 62031 MT
(which are sufficient for)84 W
/Times-Italic SF
19448 XM
(M1)SH
/Times-Roman SF
21115 XM
(to provide the)84 W
/Times-Italic SF
27172 XM
(M2)SH
/Times-Roman SF
28839 XM
(illusion. The)
418 W( mathematical relationship between)84 W
/Times-Italic SF
49090 XM
(M1)SH
/Times-Roman SF
50756 XM
(and)SH
/Times-Italic SF
9504 63317 MT
(M2)SH
/Times-Roman SF
11087 XM
(is illustrated in Figure 3-1.)SH
9504 65889 MT
(The virtual system)55 W
/Times-Italic SF
17363 XM
(M2)SH
/Times-Roman SF
19001 XM
(is truly an illusion.)56 W
/Times-Italic SF
27282 XM
(M1)SH
/Times-Roman SF
28921 XM
(describes the physical system that is composed of atomic)56 W
9504 67175 MT
(matter. The)
310 W( behavior of that physical material is not changed in)
30 W( any way by creating the illusion. All we)29 W
10800 50 9504 70352 UL
6 SS
10304 71691 MT
(5)SH
8 SS
10604 72000 MT
(Limiting the observability of these rows and columns is similar in purpose to information hiding as described in [Parnas 79].)SH
ES
%%Page: 12 14
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(12)SH
9504 7886 MT
(have done is create a new way of observing it. But we have done it)
110 W( in a way so that)111 W
/Times-Italic SF
45591 XM
(M2)SH
/Times-Roman SF
47285 XM
(appears like)111 W
9504 9172 MT
(another digital system -- i.e.,)SH
/Times-Italic SF
21225 XM
(M2\050s,t,n\051)SH
/Times-Roman SF
25141 XM
(is a function in the same form as)SH
/Times-Italic SF
38417 XM
(M1\050s,t,n\051)SH
/Times-Roman SF
(.)SH
9504 11744 MT
(By virtue of the scaling equation,)86 W
/Times-Italic SF
23602 XM
(M2)SH
/Times-Roman SF
25271 XM
(now also provides)
86 W( an accurate description of the physical system.)85 W
9504 13030 MT
(Therefore, it too, can be used as a basis for predicting accurately the physical behavior of the system.)133 W
9504 14316 MT
(This kind of scaling up can be continued for as many levels as desired,)SH
/Times-Italic SF
38027 XM
(M1, M2, M3, ..., Mn)SH
/Times-Roman SF
(.)SH
9504 16888 MT
(Examples of equations)
388 W( that scale a microprogrammable microprocessor, which is comparable in)387 W
9504 18174 MT
(complexity to a PDP 11, from gates to machine language, can be found in)
14 W( [Hunt)
SH( 87]. Equations that scale)15 W
9504 19460 MT
(a machine language program of 750 16-bit words into a simple multi-tasking operating system kernel)
45 W( are)44 W
9504 20746 MT
(described in)
14 W( [Bevier)
SH( 87a]. How this kind of scaling can be)
14 W( continued upward to define the equations for a)15 W
9504 22032 MT
(small subset of a high level programming language, Gypsy [Good 86], is described in [Bevier 87b].)SH
9504 24604 MT
(But, let's be careful. A virtual system such as)7 W
/Times-Italic SF
28238 XM
(M2)SH
/Times-Roman SF
29828 XM
(provides an)
7 W( accurate description of the physical system,)6 W
9504 25890 MT
(but does it provide a complete)
52 W( description? This depends on the actual statement of the scaling equation)53 W
9504 27176 MT
(-- i.e., on the definitions of the functions)143 W
/Times-Italic SF
27063 XM
(compose, decompose)143 W
/Times-Roman SF
36041 XM
(and)SH
/Times-Italic SF
37878 XM
(steps)SH
/Times-Roman SF
(. If)
534 W( these functions really do)142 W
9504 28462 MT
(provide an illusion that hides some)
34 W( of the observable behavior described by)35 W
/Times-Italic SF
40359 XM
(M1)SH
/Times-Roman SF
(, then)35 W
/Times-Italic SF
44234 XM
(M2)SH
/Times-Roman SF
45852 XM
(definitely is)35 W
/Times-Italic SF
50922 XM
(not)SH
/Times-Roman SF
9504 29748 MT
(a complete description.)SH
9504 32320 MT
(Does this incompleteness mean that a virtual system cannot be used to)
190 W( prove the absence of system)189 W
9504 33606 MT
(behaviors that cause physical effects?)
210 W( Again,)
671 W( this depends on the particular scaling equation. In a)211 W
9504 34892 MT
(physical digital system, some state components)
88 W( will be observable to the physical world and others will)87 W
9504 36178 MT
(not. This)
256 W( is why we connect cables to computers. For the description of a virtual system to be effective in)3 W
9504 37464 MT
(predicting the absence of a behavior that causes a physical effect,)
133 W( the scaling equation must provide a)132 W
9504 38750 MT
(complete description)127 W
/Times-Italic SF
18368 XM
(only)SH
/Times-Roman SF
20467 XM
(of those state components that are observable to the physical world.)
127 W( But,)
505 W( it)128 W
/Times-Italic SF
9504 40036 MT
(must)SH
/Times-Roman SF
11643 XM
(describe accurately)SH
/Times-Italic SF
19584 XM
(every)SH
/Times-Roman SF
21999 XM
(state component that)SH
/Times-Italic SF
30526 XM
(is)SH
/Times-Roman SF
31443 XM
(physically observable.)SH
11 /Times-Bold AF
9504 42933 MT
(3.4.2 Objectives)
275 W( for Scaling)SH
10 /Times-Roman AF
9504 45271 MT
(Scaling equations can be used to scale an accurate mathematical description)
75 W( of a physical digital system)74 W
9504 46557 MT
(from gates to micro code to machine language)
203 W( to an operating system to a high level programming)204 W
9504 47843 MT
(language. It)
354 W( is useful)
52 W( to consider what that particular scaling needs to accomplish to reduce the apparent)51 W
9504 49129 MT
(complexity of the physical system. Let us return to the issue of limiting the observability of the rows and)28 W
9504 50415 MT
(columns in Table 3-1.)SH
9504 52987 MT
(The length of a row is the number of observable state transitions. Reducing this)
158 W( number is what we)157 W
9504 54273 MT
(attempt to do with higher level control)
222 W( structures. We attempt to deny the observability of certain)223 W
8 SS
38500 55214 MT
(6)SH
10 SS
9504 55559 MT
(intermediate state transitions. Sometimes we succeed. Often we do not.)SH
9504 58131 MT
(The length of a column is the number of observable)
13 W( state components. Reducing this number is more of a)14 W
9504 59417 MT
(challenge.)SH
9504 61989 MT
(We can start by making those bits that are not relevant to a particular)
47 W( computation unobservable. This is)46 W
9504 63275 MT
(the strategy)
109 W( of)110 W
/Times-Italic SF
15804 XM
(separation)SH
/Times-Roman SF
(. We)
470 W( attempt to partition the system state so that, over a particular period of)110 W
9504 64561 MT
(time, the behavior of one set of state components is completely independent of another)
35 W( set. For example,)34 W
9504 65847 MT
(if we can partition the state into two completely different sets of size)24 W
/Times-Italic SF
37506 XM
(p)SH
/Times-Roman SF
38280 XM
(and)SH
/Times-Italic SF
39998 XM
(q)SH
/Times-Roman SF
40772 XM
(so that)
24 W( the behavior of those)25 W
9504 67133 MT
(two partitions have absolutely no effect on each other, then we only have)
203 W( 2^\050p*n\051+2^\050q*n\051 possible)202 W
10800 50 9504 69428 UL
6 SS
10304 70767 MT
(6)SH
8 SS
10604 71076 MT
(Control structures that make visible only those states that satisfy known)
184 W( mathematical relationships provide a particularly)183 W
9504 72000 MT
(effective basis for mathematical analysis [Dijkstra 76, Hoare 85].)SH
ES
%%Page: 13 15
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(13)SH
9504 7886 MT
(behaviors instead of 2^\050p*n\051*2^\050q*n\051. Divide and)
56 W( conquer works! This separation strategy is familiar in)57 W
9504 9172 MT
(operating systems. It also is achieved in higher level)
125 W( programming languages with varying degrees of)124 W
9504 10458 MT
(success.)SH
9504 13030 MT
(What else)
51 W( can we do to reduce the number of observable state components? We can group sets of)52 W
/Times-Italic SF
49953 XM
(n)SH
/Times-Roman SF
50755 XM
(bits)SH
9504 14316 MT
(together in ways so that they have less than)81 W
/Times-Italic SF
27814 XM
(2^n)SH
/Times-Roman SF
29566 XM
(values. This)
410 W( means creating equivalence classes. If we)80 W
9504 15602 MT
(take the five state components in Table 3-1 and group them)
37 W( into an equivalence class with just 20 values,)38 W
9504 16888 MT
(instead of 32,)
96 W( the number of possible behaviors reduces from 32^7\050=3.43*10^10\051 to 20^7\050=1.28*10^9\051.)95 W
9504 18174 MT
(Again, this effect is achieved in higher level programming languages with varying degrees of success.)SH
9504 20746 MT
(Truly effective, mathematically rigorous solutions to)
224 W( these problems have yet to be found, but they)225 W
9504 22032 MT
(indicate important objectives for the design of operating)
369 W( systems and higher level programming)368 W
9504 23318 MT
(languages. We)
484 W( can)
117 W( scale up, but scaling needs to have a purpose. Reducing apparent complexity is a)118 W
9504 24604 MT
(good one.)SH
ES
%%Page: 14 16
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(14)SH
13 /Times-Bold AF
28053 15271 MT
(Chapter 4)SH
19979 17530 MT
(ENGINEERING DIGITAL SYSTEMS)SH
10 /Times-Roman AF
9504 25416 MT
(The scientific and mathematical foundations that are)
162 W( needed to advance the practice of digital system)161 W
9504 26702 MT
(engineering are simple to state. Digital system engineers need equations that accurately and completely)80 W
9504 27988 MT
(describe the behavior of the physical system they are going)
75 W( to install in the real world of atomic matter.)74 W
9504 29274 MT
(They need equations that describe the higher level virtual)
262 W( systems that they will be using on that)263 W
9504 30560 MT
(computer. They)
250 W( need mathematics to apply the equations.)SH
12 /Times-Bold AF
9504 34244 MT
(4.1 Future)
300 W( Practice)SH
10 /Times-Roman AF
9504 36714 MT
(Let's take a look at what digital system engineering based on these foundations might be like.)SH
9504 39286 MT
(The primary value of these foundations is that it enables a digital)
27 W( system engineer to analyze the behavior)26 W
9504 40572 MT
(of a system)29 W
/Times-Italic SF
14396 XM
(before)SH
/Times-Roman SF
17231 XM
(it actually is constructed. This provides a rigorous, objective way of making informed)30 W
9504 41858 MT
(design and implementation decisions. An engineer can make much)
1 W( better informed decisions because s/he)SH
9504 43144 MT
(can determine accurately what the effects of various decisions will be.)
94 W( Such)
439 W( information is essential to)95 W
9504 44430 MT
(building a system to given specifications within given resource limitations.)SH
9504 47002 MT
(Digital system engineering based on these)
48 W( foundations would involve many applications of the following)47 W
9504 48288 MT
(three steps:)SH
11504 49627 MT
(1.)SH
12504 XM
(Identify a mathematical function, such)
294 W( as)295 W
/Times-Italic SF
31017 XM
(M\050s,t,n\051)SH
/Times-Roman SF
(, that describes the behavior of the)295 W
12504 50732 MT
(physical or virtual system in question.)SH
11504 52490 MT
(2.)SH
12504 XM
(Identify an acceptance test)298 W
/Times-Italic SF
24580 XM
(A\050M\050s,t,n\051\051)SH
/Times-Roman SF
29570 XM
(that conclusively distinguishes acceptable from)297 W
12504 53595 MT
(unacceptable behavior.)SH
11504 55353 MT
(3.)SH
12504 XM
(Mathematically demonstrate that system behaviors pass the acceptance test.)SH
9504 57925 MT
(The application of)
47 W( these steps would begin in the construction of computer hardware. The main goals of)48 W
9504 59211 MT
(the hardware engineering would be to)
162 W( provide, at reasonable cost, digital systems in which electronic)161 W
9504 60497 MT
(behavior conformed to a particular mathematical function, such as)155 W
/Times-Italic SF
37671 XM
(M\050s,t,n\051)SH
/Times-Roman SF
(,)SH
/Times-Italic SF
41492 XM
(and)SH
/Times-Roman SF
43397 XM
(to tell the rest of)
155 W( the)156 W
9504 61783 MT
(world exactly what that function)
172 W( is. Hardware engineering also would be responsible for developing)171 W
9504 63069 MT
(methods for testing and maintaining the physical computing system so that its behavior will conform)
89 W( to)90 W
9504 64355 MT
(the mathematical function.)SH
9504 66927 MT
(Operating systems and programming languages also)
31 W( will need to identify the mathematical functions they)30 W
9504 68213 MT
(provide. Only)
470 W( in this way can a software engineer build programs in which computer behavior can)
110 W( be)111 W
9504 69499 MT
(predicted accurately. This will require a rigorous mathematical definition of operating systems and)225 W
9504 70785 MT
(programming languages, and it will require rigorous mathematical demonstrations that)
316 W( the scaling)317 W
ES
%%Page: 15 17
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(15)SH
9504 7886 MT
(equations are satisfied.)SH
9504 10458 MT
(Based on these)
57 W( foundations, a software engineer will be able to make rigorous, objective decisions about)56 W
9504 11744 MT
(alternative software design and implementation)
91 W( questions. Making these decisions will be based on the)92 W
9504 13030 MT
(mathematical analysis of alternative program structures. This analysis will be based)
161 W( on mathematical)160 W
9504 14316 MT
(evaluation rather than on physical testing. This analysis will be performed on the)
54 W( program text, possibly)55 W
9504 15602 MT
(with the aid)
68 W( of mechanical tools that amplify the engineer's ability to perform the mathematical analysis)67 W
9504 16888 MT
(and reduce the probability of human analytical error.)SH
9504 19460 MT
(There is much research and development that needs to be done)
108 W( to reach the point where digital system)109 W
9504 20746 MT
(engineers routinely can apply this kind of mathematics to constructing systems. To put it)
134 W( bluntly, the)133 W
9504 22032 MT
(mathematical foundations and)
57 W( methods still need to be developed. Effective means for applying them in)58 W
9504 23318 MT
(engineering practice also need to be developed, implemented and adopted.)
27 W( We)
303 W( also need to start thinking)26 W
9504 24604 MT
(about designing hardware, operating systems and)
287 W( programming languages to facilitate this kind of)288 W
9504 25890 MT
(mathematical analysis. We need to)
152 W( discover the most effective kinds of mathematical functions upon)151 W
9504 27176 MT
(which to base that design. We also need to discover acceptance tests that distinguish acceptable)
129 W( from)130 W
9504 28462 MT
(unacceptable behavior for various kinds of systems.)SH
12 /Times-Bold AF
9504 32146 MT
(4.2 Current)
300 W( Practice)SH
10 /Times-Roman AF
9504 34616 MT
(The current practice of digital system engineering is far removed from practice that)
93 W( is based on science)92 W
9504 35902 MT
(and mathematics. It is instructive)
213 W( to think about how far removed it really is. Let me pose some)214 W
9504 37188 MT
(questions.)SH
9504 39760 MT
(What kind of information is there that describes the physical behavior of the computer systems that are)96 W
9504 41046 MT
(operating today and causing effects in our physical environment? Does)
46 W( this information describe exactly)47 W
9504 42332 MT
(and completely what next state will be produced from the current state and how)
68 W( long it will take? Does)67 W
9504 43618 MT
(the accuracy and precision of this information approach that of a mathematical function such as)SH
/Times-Italic SF
47968 XM
(M\050s,t,n\051)SH
/Times-Roman SF
(?)SH
9504 46190 MT
(Consider the information about computer system behavior)
6 W( that a hardware engineer typically provides to a)7 W
9504 47476 MT
(software engineer. What is it? It's a reference manual. How close does)
150 W( that information come to a)149 W
9504 48762 MT
(mathematical function that is a complete description of the physical behavior of the)
134 W( system? If we're)135 W
9504 50048 MT
(going to make accurate statements that hardware will not cause harmful effects, we need to know)
39 W( exactly)38 W
9504 51334 MT
(what happens to every observable bit in the)
80 W( system on every observable state transition, and we need to)81 W
9504 52620 MT
(know how long it takes. Does the hardware engineer even know)
262 W( what mathematical function the)261 W
9504 53906 MT
(hardware)SH
/Times-Italic SF
13591 XM
(does)SH
/Times-Roman SF
15791 XM
(provide to the software engineer? Doesn't this leave the software engineer in)
117 W( the same)118 W
9504 55192 MT
(position as having first to)SH
/Times-Italic SF
19921 XM
(discover)SH
/Times-Roman SF
23559 XM
(Ohm's Law before s/he can even begin to think about)SH
/Times-Italic SF
45277 XM
(applying)SH
/Times-Roman SF
49027 XM
(it?)SH
9504 57764 MT
(What kind of information does a software engineer have? More manuals.)
239 W( Programming)
726 W( language)238 W
9504 59050 MT
(manuals! These)
264 W( languages range)
7 W( from the micro code level on up to the "Higher Order Languages." How)8 W
9504 60336 MT
(many of these manuals describe exactly the next observable state the physical machine will produce from)34 W
9504 61622 MT
(the current one? How many tell how long it will take? For how many programming languages is)
35 W( there a)36 W
9504 62908 MT
(mathematical function that describes accurately the behavior of its programs on a physical machine?)SH
9504 65480 MT
(How can a software engineer produce a program that makes a computer behave in a predictable)
99 W( way if)98 W
9504 66766 MT
(s/he doesn't know how the program will make)
20 W( the computer behave? We're going to use Ada to program)21 W
9504 68052 MT
(systems with predictable real-time behavior. Right!)SH
9504 70624 MT
(How many engineers identify any kind of objectively measurable acceptance test criteria for a)
114 W( system?)113 W
9504 71910 MT
(Do the criteria distinguish conclusively)
109 W( between acceptable and unacceptable for every possible system)110 W
ES
%%Page: 16 18
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(16)SH
9504 7886 MT
(behavior? How)
576 W( can)
163 W( anyone predict that the future behavior of a computer system will be acceptable)162 W
9504 9172 MT
(without identifying the limits of acceptability?)SH
9504 11744 MT
(How many engineers use any kind of mathematical analysis to demonstrate that their)
141 W( systems pass an)142 W
9504 13030 MT
(acceptance test? How can they, without mathematical functions)
144 W( that describe system behavior and an)143 W
9504 14316 MT
(acceptance test?)SH
9504 16888 MT
(Current engineering practice is based)
95 W( primarily on physical testing. Exhaustive testing is practical only)96 W
9504 18174 MT
(for the tiniest of systems. On larger systems, how often is any kind of systematic statistical testing done?)SH
9504 20746 MT
(Software engineering practice is in a very immature state. Our expectations far exceed our capabilities.)86 W
9504 22032 MT
(In many cases, we can't even be)
105 W( precise about what our expectations are. Often, even though we may)106 W
9504 23318 MT
(have 25 pounds of requirements documentation,)
15 W( we simply do not know what we want a computer system)14 W
9504 24604 MT
(to do! So, because it's so much fun to build these systems and watch them do something, we just build)71 W
8 SS
26961 25545 MT
(7)SH
10 SS
9504 25890 MT
(them and see if they do something we like.)40 W
27651 XM
(Often they do. However, sometimes they)
40 W( also do something)39 W
9504 27176 MT
(we did not foresee and cause harmful effects.)SH
9504 29748 MT
(This sandbox engineering practice can)
6 W( carry us only so far. When applied to systems that can cause major)7 W
9504 31034 MT
(effects in our physical environment, it's)
29 W( only a matter of time before it carries us into real, physical harm.)28 W
9504 32320 MT
(For some, it already has.)SH
10800 50 9504 66656 UL
6 SS
10304 67995 MT
(7)SH
8 SS
10604 68304 MT
(One of the things that encourages this kind of practice is that the raw materials that programs are)
31 W( composed of are free! No one)30 W
9504 69228 MT
(charges for assignment statements. Just get a new one out of an endless warehouse.)
24 W( The)
249 W( only thing that's going to cost anyone any)25 W
9504 70152 MT
(money is "just" the cost of someone's labor to hook it up with other assignment statements and stuff.)
75 W( Most)
348 W( other engineer fields)74 W
9504 71076 MT
(don't have this "blessing." I suspect one of the reasons the Empire State building was built only once)
33 W( was that someone had to pay)34 W
9504 72000 MT
(for concrete and steel.)SH
ES
%%Page: 17 19
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(17)SH
13 /Times-Bold AF
28053 15271 MT
(Chapter 5)SH
26445 17530 MT
(CONCLUSION)SH
10 /Times-Roman AF
9504 25416 MT
(Science and mathematics are not required to engineer physical systems, but they sure do help!)
181 W( Pre-)614 W
9504 26702 MT
(historic engineers built bridges by laying stones and logs across a stream.)
218 W( But)
684 W( it took science and)217 W
9504 27988 MT
(mathematics to build the Golden Gate. Benjamin Franklin)
240 W( was able to go fly a kite and discover)241 W
9504 29274 MT
(electricity. But,)
399 W( how many electrical systems were engineered successfully without Ohm's Law and the)74 W
9504 30560 MT
(mathematics to apply it?)SH
9504 33132 MT
(What is the Ohm's Law of)
52 W( digital system engineering? It is the mathematical function that describes the)53 W
9504 34418 MT
(physical behavior of a digital computer. From science, we need to identify the mathematical)
108 W( functions)107 W
9504 35704 MT
(that describe accurately and completely the physical behavior of)
38 W( computers. From mathematics, we need)39 W
9504 36990 MT
(the ability to apply these functions effectively. Without these foundations, the capabilities)
189 W( of digital)188 W
9504 38276 MT
(system engineering will remain very limited.)SH
9504 40848 MT
(A good engineer)
150 W( must do the best s/he can with what s/he has. An engineer builds the best possible)151 W
9504 42134 MT
(product from the resources that are available. A wise engineer will not try)
7 W( to engineer systems beyond the)6 W
9504 43420 MT
(limits of available technology.)SH
9504 45992 MT
(Stones and logs have carried many a person safely from one)
174 W( side of a stream to another. For some)175 W
9504 47278 MT
(purposes, that was, and still is, good, sound technology. The physical laws of nature)
79 W( have not changed.)78 W
9504 48564 MT
(But, when pushed beyond its limits, to try to get across some water that was too swift or too wide)
53 W( or too)54 W
9504 49850 MT
(deep, this technology presents a real, physical danger.)SH
9504 52422 MT
(Digital system engineering is already)
60 W( pushing beyond the limits of available technology. It is limited by)59 W
9504 53708 MT
(the absence of scientific and mathematical foundations.)
105 W( Without)
461 W( them, digital systems will continue to)106 W
9504 54994 MT
(have unpredictable)
130 W( behavior that will cause physical harm. What harm will be caused will depend on)129 W
9504 56280 MT
(what physical effects a digital system is allowed to control.)SH
ES
%%Page: 18 20
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(18)SH
13 /Times-Bold AF
25471 8071 MT
(Acknowledgements)SH
10 /Times-Roman AF
9504 12357 MT
(Many of the observations I have made here have been made by others. What I have done)
6 W( is interpret them)7 W
9504 13643 MT
(from the)
48 W( view that computing is a physical science, just like physics or chemistry. It matters not that the)47 W
9504 14929 MT
(object of study, a computer, is the product of a manufacturing process.)
75 W( A)
401 W( computer is still a part of the)76 W
9504 16215 MT
(physical world of atomic)
83 W( particles. The laws of nature still apply. The manufacturing process does not)82 W
9504 17501 MT
(suspend them. The most effective way we have to predict the behavior)
173 W( of the physical world is the)174 W
9504 18787 MT
(traditional scientific method. Discover the mathematical equations that describe the object of study, and)66 W
9504 20073 MT
(apply them to predict its physical behavior.)SH
9504 22645 MT
(I am particularly indebted to J Moore, Warren)
39 W( Hunt, Bill Bevier and Bill Young for surrounding me with)40 W
9504 23931 MT
(a mountain of proved mathematical statements about computer hardware, operating systems and)377 W
9504 25217 MT
(programming languages, and to Bob Boyer and J Moore's wonderful deduction machine)
22 W( [Boyer)
SH( & Moore)22 W
9504 26503 MT
(88] that was used to)
137 W( build that mountain. The scaling equations that I have presented primarily are a)136 W
9504 27789 MT
(result of that work.)SH
9504 30361 MT
(I especially thank Bob Morris for insisting that I think)
7 W( about silicon. This was the catalyst from which my)8 W
9504 31647 MT
(view of computing as a physical science emerged.)SH
9504 34219 MT
(This paper)
186 W( also appears in the Proceedings of COMPASS '88 \0503rd Annual Conference on Computer)185 W
9504 35505 MT
(Assurance\051.)SH
ES
%%Page: 19 21
BS
0 SI
10 /Times-Roman AF
51200 4286 MT
(19)SH
13 /Times-Bold AF
27820 8071 MT
(References)SH
10 /Times-Roman AF
9504 10444 MT
([Bevier 87a])SH
17004 XM
(William R. Bevier.)SH
/Times-Italic SF
17004 11549 MT
(A Verified Operating System Kernel)SH
/Times-Roman SF
(.)SH
17004 12654 MT
(Technical Report CLI-11, Computational Logic, Inc., October, 1987.)SH
17004 13759 MT
(Also Ph.D. Thesis, The University of Texas at Austin, 1987.)SH
9504 15550 MT
([Bevier 87b])SH
17004 XM
(William R. Bevier, Warren A. Hunt, Jr., and William D. Young.)SH
/Times-Italic SF
17004 16655 MT
(Toward Verified Execution Environments)SH
/Times-Roman SF
(.)SH
17004 17760 MT
(Technical Report CLI-5, Computational Logic, Inc., 1987.)SH
17004 18865 MT
(Also appears in "Proceedings of the 1987 IEEE Symposium on Security and Privacy".)SH
9504 20656 MT
([Boyer & Moore 88])SH
17004 21761 MT
(Robert S. Boyer, J Strother Moore.)SH
/Times-Italic SF
17004 22866 MT
(The User's Manual for A Computational Logic)SH
/Times-Roman SF
(.)SH
17004 23971 MT
(Technical Report CLI-18, Computational Logic, Inc., February, 1988.)SH
9504 25762 MT
([Dahl 72])SH
17004 XM
(E.W. Dijkstra.)SH
17004 26867 MT
(Notes on Structured Programming.)SH
/Times-Italic SF
17004 27972 MT
(Structured Programming.)SH
/Times-Roman SF
17004 29077 MT
(Academic Press, 1972.)SH
9504 30868 MT
([Dijkstra 76])SH
17004 XM
(E.W. Dijkstra.)SH
/Times-Italic SF
17004 31973 MT
(A Discipline of Programming.)SH
/Times-Roman SF
17004 33078 MT
(Prentice-Hall, 1976.)SH
9504 34869 MT
([Good 86])SH
17004 XM
(Donald I. Good, Robert L. Akers, Lawrence M. Smith.)SH
/Times-Italic SF
17004 35974 MT
(Report on Gypsy 2.05 - January 1986)SH
/Times-Roman SF
17004 37079 MT
(Computational Logic, Inc., 1986.)SH
9504 38870 MT
([Goodenough & Gerhart 75])SH
17004 39975 MT
(J. B. Goodenough and S. L. Gerhart.)SH
17004 41080 MT
(Toward a theory of test data selection.)SH
/Times-Italic SF
17004 42185 MT
(IEEE Trans. on Software Engineering)SH
/Times-Roman SF
32504 XM
(2, June, 1975.)SH
9504 43976 MT
([Hayes 87])SH
17004 XM
(Ian Hayes \050Editor\051.)SH
/Times-Italic SF
17004 45081 MT
(Specification Case Studies.)SH
/Times-Roman SF
17004 46186 MT
(Prentice-Hall, 1987.)SH
9504 47977 MT
([Hoare 85])SH
17004 XM
(C. A. R. Hoare.)SH
17004 49082 MT
(Programs are Predicates.)SH
/Times-Italic SF
17004 50187 MT
(Mathematical Logic and Programming Languages.)SH
/Times-Roman SF
17004 51292 MT
(Prentice Hall International Series in Computer Science., 1985.)SH
9504 53083 MT
([Hunt 87])SH
17004 XM
(Warren A. Hunt, Jr.)SH
/Times-Italic SF
17004 54188 MT
(The Mechanical Verification of a Microprocessor Design)SH
/Times-Roman SF
(.)SH
17004 55293 MT
(Technical Report CLI-6, Computational Logic, Inc., 1987.)SH
17004 56398 MT
(See also "FM8501: A Verified Microprocessor", Ph. D. Thesis, The University of)SH
18504 57503 MT
(Texas at Austin, 1985.)SH
9504 59294 MT
([Leveson 86])SH
17004 XM
(Nancy G. Leveson.)SH
17004 60399 MT
(Software Safety: Why, What, and How.)SH
/Times-Italic SF
17004 61504 MT
(ACM Computing Surveys)SH
/Times-Roman SF
27420 XM
(18,2, June, 1986.)SH
9504 63295 MT
([Parnas 79])SH
17004 XM
(D.L. Parnas.)SH
17004 64400 MT
(Designing Software for Ease of Extension and Contraction.)SH
/Times-Italic SF
17004 65505 MT
(IEEE Transactions on Software Engineering)SH
/Times-Roman SF
35143 XM
(5-2, March, 1979.)SH
ES
%%Page: i 22
BS
0 SI
13 /Times-Bold AF
26229 11604 MT
(Table of Contents)SH
12 /Times-Roman AF
9504 16027 MT
(Chapter 1. Introduction)
SH( .)
165 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(1)SH
9504 19222 MT
(Chapter 2. Science, Mathematics and Engineering)
SH( .)
565 W( . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(2)SH
9504 22417 MT
(Chapter 3. Mathematics for Digital Systems)
SH( .)
461 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51600 XM
(4)SH
11 SS
11704 24458 MT
(3.1. Describing System Behavior)
SH( .)
277 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51650 XM
(4)SH
10 SS
12504 25563 MT
(3.1.1. Completeness)
SH( .)
389 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(5)SH
12504 26668 MT
(3.1.2. Magnitude)
SH( .)
167 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(6)SH
12504 27773 MT
(3.1.3. Instability)
SH( .)
444 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(6)SH
11 SS
11704 28969 MT
(3.2. Defining Acceptable Behavior)
SH( .)
37 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51650 XM
(7)SH
11704 30165 MT
(3.3. Demonstrating Acceptable Behavior)
SH( .)
159 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51650 XM
(8)SH
10 SS
12504 31270 MT
(3.3.1. Enumeration)
SH( .)
334 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51700 XM
(8)SH
12504 32375 MT
(3.3.2. Probabilistic Analysis)
SH( .)
194 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51200 XM
(10)SH
12504 33480 MT
(3.3.3. Deduction)
SH( .)
334 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51200 XM
(10)SH
11 SS
11704 34676 MT
(3.4. Scaling Up)
SH( .)
306 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51100 XM
(10)SH
10 SS
12504 35781 MT
(3.4.1. Equations for Scaling)
SH( .)
334 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51200 XM
(11)SH
12504 36886 MT
(3.4.2. Objectives for Scaling)
SH( .)
57 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51200 XM
(12)SH
12 SS
9504 40081 MT
(Chapter 4. Engineering Digital Systems)
SH( .)
96 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51000 XM
(14)SH
11 SS
11704 42122 MT
(4.1. Future Practice)
SH( .)
186 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51100 XM
(14)SH
11704 43318 MT
(4.2. Current Practice)
SH( .)
248 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51100 XM
(15)SH
12 SS
9504 46513 MT
(Chapter 5. Conclusion)
SH( .)
32 W( . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .)SH
51000 XM
(17)SH
10 SS
30713 75600 MT
(i)SH
ES
%%Page: ii 23
BS
0 SI
10 /Times-Roman AF
27907 7886 MT
(List of Figures)SH
/Times-Bold SF
9504 17801 MT
(Figure 2-1:)SH
/Times-Roman SF
15253 XM
(Science and Mathematics)SH
51700 XM
(2)SH
/Times-Bold SF
9504 19592 MT
(Figure 3-1:)SH
/Times-Roman SF
15253 XM
(Virtual System)SH
51200 XM
(11)SH
30574 75600 MT
(ii)SH
ES
%%Page: iii 24
BS
0 SI
10 /Times-Roman AF
28074 7886 MT
(List of Tables)SH
/Times-Bold SF
9504 17801 MT
(Table 3-1:)SH
/Times-Roman SF
14865 XM
(Example Behavior)SH
51700 XM
(5)SH
30435 75600 MT
(iii)SH
ES
%%Trailer
%%Pages: 24
%%DocumentFonts: Times-Roman Times-Bold Symbol Times-Italic Courier-Bold