Software Requirements Specification And Analysis Using Zed .

GCS Development Specification as the “B5[19].” Howeverthe B5 clearly states that it is one part of the life cycle datarequired to fulfill the RTCS/DO178A. In Version 2.2 ofthe B5, it is clear that this data is considered to be the“Software Requirements” document. While in the Version2.3 of the B5 (which refers to Version B of RTCS/DO178),the wording “Software Requirements” have been removed.In any case, we used Version 2.2 (with Mods 1-8).5METHODS APPLICATIONOur experiment focused on applying the methods describedabove to the Altimeter Radar Sensor Processing (ARSP)module of the Guidance and Control Software (GCS)Development Specification [18]. The GCS, an embeddedreal-time software system, is at the heart of the VikingMars Lander. This system was designed to providesoftware control of the embedded sensors and actuatorsduring the terminal decent phase of the Viking Marsmission. The ARSP module reads data provided by thealtimeter radar sensor to determine the lander’s altitudefrom the Mars surface.The ARSP module is provided below exactly as itappears within the complete GCS specification [18, 20].INPUTAR ALTITUDEAR FREQUENCYFRAME COUNTERThe NL specification for the ARSP module, a part of theGCS, is the starting point in this study. Figure 1 shows thelocation of the ARSP module in the entire GCS system.The next step transformed the B5 into Zed as a concretespecification form. Zed is thus presented as an intermediatestep. Subsequently, the ARSP was represented (andevaluated) as Statecharts and activity-charts. The outcomefrom this evaluation is therefore described below as thefinal result of our analysis.OUTPUTAR ALTITUDEK ALTGSPTSPARSPTDLRSPASPSENSOR OUTPUTGPRUN PARAMETERSGUIDANCE STATECRCPAECLPCONTROL ANDTELEMETRYOUTPUTSAR STATUSPROCESS:It is only necessary that this functional module performits normal calculations every other frame, namely on theodd-numbered frames; however, it is required that thisfunctional module execute every frame. The reason forthis is that during its normal processing it must rotatehistory variables. This means that during the frameswhen it does not need to calculate new outputs, namelythe even-numbered frames, it must still rotate its historyvariables and set its new or current values equal to theprevious values, thus creating double entries for eachrotated variable. By doubling the entries, consistency oftime histories will be maintained at the expense ofkeeping two copies of each value in these variables, andforcing the functional module to execute every frame.SENSOR DATAASPAR COUNTERAR STATUSK ALTThe processing of the altimeter counter data(AR COUNTER) into the vehicle's altitude above theplanet's terrain depends on whether or not an echo isreceived by the altimeter radar for the current time step.The distance covered by the radio pulses emitted from thealtimeter radar is directly proportional to the timebetween transmission and reception of its echo. A digitalcounter (AR COUNTER) is started as the radar pulse istransmitted. The counter increments AR FREQUENCYtimes per second. If an echo is received, the lower orderfifteen bits of AR COUNTER contain the pulse count, andthe sign bit will contain the value zero. If an echo is notreceived, AR COUNTER will contain sixteen one bits.RECLPPACKETCPFigure 1 Process 2. RUN GCS5.1B5 – THE NL BASED SPECIFICATIONThe GCS Development Specification indicates that it wasdeveloped based on the RTCA/DO178A. The DO178provides guidelines for Software Considerations InAirborne System and Equipment Certification. It does notprovide any standards (recommended practice/guidelines)concerning the actual requirements specification of thesoftware unlike the IEEE Std 830-1998. The IEEEstandard outlines the specific material and format needed.The GCS however has a concrete and systematic formatthat it uses to present its content. The format is resemblesthe old B5 style format used in various Military projectsduring the Cold War. Hence, we choose to refer to the3 ROTATE VARIABLESRotate AR ALTITUDE, AR STATUS, and K ALT. PERFORM ALTERNATE PROCESSING:If FRAME COUNTER is an even number, insure thatthe current values of AR ALTITUDE, AR STATUS,and K ALT are equal to the previous values ofAR ALTITUDE,AR STATUS,andK ALTrespectively.

DETERMINE ALTITUDE:a. If an echo is received,direction of the variables is unclear. The second issueconcerns the type assigned to the AR COUNTER variable.Issue number three is about the fact that an undefined 3rdorder polynomial is used to determine the AR ALTITUDEvalue. Finally, there is some question about where theAR COUNTER should be modified.Convert the AR COUNTER value to a distance tobe returned in the variable AR ALTITUDEaccording to the following equation:Equation 1: AR ALTITUDE Element calculationAR ALTITUDE Three variables are identified that are to be rotated. Inthis context, it could mean exchanging the values amongoneanother(e.g.,Temp: AR ALTITUDE,AR ALTITUDE: AR STATUS, etc.) or as was assumedin the Zed version (Fig. 5), rotation occurs within thevariable since each variable is a four element array.8 msecAR FREQUENCY 2AR COUNTER 3 10b. If an echo is not received, compute AR ALTITUDEas follows:1) If all four previous values of AR STATUS arehealthy:As explained above, the AR STATUS, AR ALTITUDE,and K ALT array element values are rotated. The rotationdirection could be left shift or right shift. We decided toshift the array element to the right. In Figure 2, “New”means the currently processed value. E1 is the newest andE4 is the oldest value of the array.In order to smooth the estimate of altitude; fit athird-order polynomial to the previous four valuesof AR ALTITUDE. Use this polynomial toextrapolate a value for AR ALTITUDE for thecurrent time step.V a i a brl2) If any of the previous four values of AR STATUSis failed:E1A f t e r h e tr o t a i o ntE4wE1E2E3The B5 ARSP module specification describes theAR COUNTER as a 16-bit binary number. In the datadictionary it is described differently (i.e., as a 2-byteinteger). In the Zed version we assumed the data dictionarywas correct. In addition, a third-order polynomial is usedfor estimating the AR ALTITUDE value however nodefinition was given anywhere. Accordingly, an undefinedfunction was specified in Zed to represent the fact that sucha function is required for estimating the altitude value thatwould need to be output (i.e., AR ALTITUDE).Table 1: Determination of Altitude Status.ACTIONS TO BE TAKENAR STATUSK ALThealthyfailedfailedE3Figure 2 Variable rotation directionUPDATE STATE:Set the current values for AR STATUS and K ALTaccording to the following table.CURRENT STATEECHOAll 4 previousRETURNED? AR STATUSvalueshealthy?yesdon’t carenoyesnonoE2NeSet the current value of AR ALTITUDE equal tothe previous value of AR ALTITUDE. a r er a y110In addition, there are two confusing interpretations abouthow the AR COUNTER value is processed. In the firstinterpretation, if a timely echo (i.e., off the surface of Mars)is received from the altimeter radar then the value of theAR COUNTER is considered to be the number of pulsesfrom whence the echo was first transmitted. Otherwise, aconstant value is assumed (i.e., -1). This is not just an inputvariable but depends on the state of the radar altimeter andhence can be thought of as an internal ASRP variable.Therefore the actual value of AR COUNTER is determinedinternally as part of the ASRP processing. However, the B5gives the impression that this counter should not be updatedinside the ARSP since it is declared as an input variable!Additionally, the B5 claims that AR COUNTERaccumulates the radar pulse cycles from the time of theradar pulse transmission.Which means that theAR COUNTER value must be a positive number after thetransmission whether or not the echo is received in time.Table 1 gives the state-action constraints. In Table 1, theK ALT value is used in the Guidance Processing (GP)module to determine the correction term value ofGP ALTITUDE variable. If K ALT 0, the correctionterm is set to zero. Otherwise, a non-zero value is used inthe correction term.5.2Zed SpecificationThe Zed version of the ARSP module is shown anddescribed at length in this section [16, 21]4. There aresome issues concerning ambiguity that needed to beclarified. The first issue concerns the exact meaning (i.e.,purpose) of the rotate variables because the rotational4The "?" notation in Zed represents a variable as an input. Oneproblem was that the B5 defined variables as both input andoutput. Zed does not provide a way to describe this. So, thosevariables were treated as variables with neither "?", nor "!"notation.Given this description two possible cases wereconsidered. The first case considers the AR COUNTER to4

be updated inside the ARSP module. The other caseassumes that the AR COUNTER value is ready to be used(and will not be updated by the ARSP processing). Thefirst case is presented as a Zed specification in section5.2.1. The other case is presented in section 5.2.2.The K ALT 1, K ALT 2, K ALT 3, K ALT 4, andK ALT NEW (Sig. n, also see Table 1) variables aredefined as a set of binary elements. The AR ALTITUDE 1,AR ALTITUDE 2, AR ALTITUDE 3, AR ALTITUDE 4,and AR ALTITUDE NEW (Sig. o) are defined as a set ofreal numbers that altitude as determined by altimeter radar.AR STATUS 1,AR STATUS 2,AR STATUS 3,AR STATUS 4, and AR STATUS NEW (Sig. p) aredefined as binary values that represent health status for thevarious elements of the altimeter radar. The AR STATUS,AR ALTITUDE, and K ALT (Sigs. q-s) arrays hold theprevious 4 values of their elements respectively.5.2.1Case 1: AR COUNTER updated inside the ARSPIn case one, two conditions are considered. Because weassume the AR COUNTER value is updated within theARSP module, it should not represent the arrival of theradar echo pulse. Accordingly, a Boolean flag expressingthis condition is introduced (timely arrival or not). Todetermine the AR COUNTER value, the time between theinitial radar pulse transmission and reception of the returnecho is needed. The B5 does not distinguish the differencebetween the Boolean condition (of a timely echo arrival)and the time value represented by the counter. We believethese should be considered separately for the purpose ofclarity. The time value and the echo flag are mentionedinside of the B5 but they are not treated as separate entities.Consequently, in this study we chose to define separatevariables with the appropriate types to avoid coupling adouble meaning to one variable.The AR STATUS, AR ALTITUDE, and K ALTvariables were defined as a 4-element array in the B5specification. Zed does not have a specific array constructso these variables are designed as 4-element Cartesianproducts. The array can be also represented as a 4-elementsequence. The Cartesian product method was chosenbecause this composition assumes that any element can beaccessed directly without having to search though thesequence. The predicate u, v, and w represent thevariables ranges. The predicate x constrains the values forthe sets defined in the Signature o.ARSP RESOURCEARSP INITj Echo : {Yes, No}k FRAME COUNTER? : Nl AR FREQUENCY? : Rm AR COUNTER? : Zn K ALT 1, K ALT 2, K ALT 3, K ALT 4, K ALT NEW: {0,1}o AR ALTITUDE 1, AR ALTITUDE 2, AR ALTITUDE 3, AR ALTITUDE 4,AR ALTITUDE NEW: Rp AR STATUS 1, AR STATUS 2, AR STATUS 3, AR STATUS 4,AR STATUS NEW: {healthy, failed}q K ALT: K ALT 1 x K ALT 2 x K ALT 3 x K ALT 4jkuvFigure 4 ARSP INIT SchemaThe ARSP INIT schema (Figure 4) defines the initialstate of the ARSP module.It initializes theAR COUNTER? value to –1 meaning the radar sent out apulse but has not yet received the echo. Otherwise, theAR COUNTER? value will be updated as defined bypredicate v. The SEC (Sig. k) variable representsseconds from the point the initial radar pulse wastransmitted to the present time. It is defined inARSP INIT instead of ARSP RESOURCE because it isnot defined as an input by the B5.r AR STATUS: AR STATUS 1 x AR STATUS 2 x AR STATUS 3 xAR STATUS 4s AR ALTITUDE: AR ALTITUDE 1 x AR ALTITUDE 2 x AR ALTITUDE 3 xAR ALTITUDE 4uvwxDARSP RESOURCESEC : secondEcho No Û AR COUNTER?’ -1Echo Yes Û AR COUNTER?’ AR COUNTER? AR FREQUENCY * SECAR COUNTER? e -1.32767AR FREQUENCY? e 1.2450000000FRAME COUNTER? e 1.2147783647AR ALTITUDE 1 e 1.2000 AR ALTITUDE 2 e 1.2000 AR ALTITUDE 3 e 1.2000 AR ALTITUDE 4 e 1.2000 AR ALTITUDE NEW e 1.2000The ARSP schema (Figure 5) is the main functionalschema. The ARSP RESOURCE schema is imported forchangingintheSignaturej.TheAltitude Polynomial function (Sig. k) obtains theAR ALTITUDE as input and estimates the current altitudeby fitting a third-order polynomial to the previous value ofthe AR ALTITUDE. The AR STATUS Update (Sig. l)is a function that obtains its current value(AR STATUS NEW) and the AR STATUS as input andupdates the AR STATUS array. The K ALT Update(Sig. m) is a function that modifies the K ALT array byassigning the K ALT NEW the new value (a correctionterm needed by the guidance process).Figure 3 ARSP RESOURCE SchemaThe ARSP RESOURCE schema (Figure 3) defines theARSP module input and output variables5. Echo (Sig. j)is a Boolean variable that represents whether the returnpulse (radar echo pulse) has been received or not. TheFRAME COUNTER? (Sig. k) is an input variable givingthe present frame number and is typed as a natural number.AR FREQUENCY? (Sig. l) represents the rate at whichthe AR COUNTER? has been incremented and is typed as areal number. The AR COUNTER? (Sig. m) is an inputvariable that is used to determine the AR ALTITUDEvalue and its type is an integer.The AR ALTITUDE Update (Sig. n) is a functionthat updates the AR ALTITUDE variable by shifting the1st, 2nd, and 3rd elements value into 2nd, 3rd, and 4th elements5All data types given in the B5 are defined to satisfy theconstraints described in the data dictionary [18].5

Predicate { requires that the updates to AR STATUS andK ALT occur when FRAME COUNTER? is odd, the radarecho pulse has not yet been received, and any of theAR STATUS elements are not healthy.respectively. The current value of AR ALTITUDE NEW ispushedintothefirstelementplace.The“FRAME COUNTER? mod 2” is used to representwhether the FRAME COUNTER? values for the rest of thepredicate part are odd or even.5.2.2Case 2: AR COUNTER, the input variableIn case two, only two schemas are defined and theARSP RESOURCE schema of this case is different than inthe case one (i.e., the Echo variable is not included). Also,the case one ARSP INIT schema is not needed. The onlyassumption in this case is that the AR COUNTER valuemust be updated from outside of the ARSP module and isready for immediate use. When the AR COUNTER value is–1 this indicates that the echo of the radar pulse has not yetbeen received. If the AR COUNTER value is a positiveinteger, it means that the echo of the radar pulse arrived atthe time indicated by the value of the counter.ARSPj D ARSP RESOURCEk Altitude Polynomial: AR ALTITUDE f Rl AR STATUS Update: AR STATUS NEW x AR STATUS f AR STATUSm K ALT Update: K ALT NEW x K ALT f K ALTn AR ALTITUDE Update: AR ALTITUDE NEW x AR ALTITUDE fAR ALTITUDEu FRAME COUNTER? mod 2 0 Û AR ALTITUDE’ AR ALTITUDE Update(AR ALTITUDE 1, AR ALTITUDE) AR STATUS’ AR STATUS Update (AR STATUS 1, AR STATUS) K ALT’ K ALT Update (K ALT 1, K ALT)v FRAME COUNTER? mod 2 1 Echo Yes Û AR ALTITUDE’ AR ALTITUDE Update(AR COUNTER? * 300000000 divAR FREQUENCY div 2, AR ALTITUDE)w FRAME COUNTER? mod 2 1 Echo No AR STATUS (healthy,healthy, healthy, healthy)ÛAR ALTITUDE’ AR ALTITUDE Update(Altitude PolynomialAR ALTITUDE, AR ALTITUDE)x FRAME COUNTER? mod 2 1 Echo No AR STATUS ë(healthy,healthy, healthy, healthy)ÛAR ALTITUDE’ AR ALTITUDE Update (AR ALTITUDE 1,AR ALTITUDE)y FRAME COUNTER? mod 2 1 Echo Yes Û AR STATUS’ AR STATUS Update(healthy, AR STATUS) K ALT’ K ALT Update(1, K ALT)z FRAME COUNTER? mod 2 1 Echo No AR STATUS (healthy,healthy, healthy, healthy)Û AR STATUS’ AR STATUS Update(failed, AR STATUS) K ALT’ K ALT Update(1, K ALT){ FRAME COUNTER? mod 2 1 Echo No AR STATUS ë (healthy,healthy, healthy, healthy)Û AR STATUS’ AR STATUS Update(failed, AR STATUS) K ALT’ K ALT Update(0, K ALT)The ARSP RESOURCE schema (Figure 6) defines theinput and output variables for the ARSP module. All of theZed data types were defined based on their data dictionaryentry in the B5 [18]. The FRAME COUNTER? (Sig. j) andthe AR FREQUENCY? (Sig. k) are defined the same as incase one (no need to repeat here).However, theAR COUNTER? (Sig. l) is an input variable that containsthe counter value of elapsed time from the time of theinitial radar pulse transmission toward Mars.ARSP RESOURCEj FRAME COUNTER? : Nk AR FREQUENCY? : Rl AR COUNTER? : Zm K ALT 1, K ALT 2, K ALT 3, K ALT 4, K ALT NEW: {0,1}n AR ALTITUDE 1, AR ALTITUDE 2, AR ALTITUDE 3, AR ALTITUDE 4,AR ALTITUDE NEW: Ro AR STATUS 1, AR STATUS 2, AR STATUS 3, AR STATUS 4,AR STATUS NEW: {healthy, failed}p K ALT: K ALT 1 x K ALT 2 x K ALT 3 x K ALT 4Figure 5 ARSP SchemaPredicate u requires that the current AR ALTITUDE,AR STATUS, and K ALT values remain the same as theirprevious value when the FRAME COUNTER? is even.Predicate v defines the AR ALTITUDE update. Theupdate takes the current value calculated by Equation 1when FRAME COUNTER? is odd and the radar pulse echohas arrived on time.q AR STATUS: AR STATUS 1 x AR STATUS 2 x AR STATUS 3 xAR STATUS 4r AR ALTITUDE: AR ALTITUDE 1 x AR ALTITUDE 2 x AR ALTITUDE 3 xAR ALTITUDE 4u AR COUNTER? e -1.32767v AR FREQUENCY? e 1.2450000000w FRAME COUNTER? e 1.2147483647Predicate w requires that newest AR ALTITUDE value beestimated by the Altitude Polynomial functionwhen the FRAME COUNTER? is odd, the radar echo pulsedid not arrive on time, and all AR STATUS elements arehealthy.x AR ALTITUDE 1 e 1.2000 AR ALTITUDE 2 e 1.2000 AR ALTITUDE 3 e 1.2000 AR ALTITUDE 4 e 1.2000 AR ALTITUDE NEW e 1.2000Figure 6 ARSP RESOURCE schemaPredicate x requires that the newest AR ALTITUDE valuebe the same as the previous value whenFRAME COUNTER? is odd, the radar pulse echo did notarrive, and any of the AR STATUS elements are nothealthy.The K ALT 1, K ALT 2, K ALT 3, K ALT 4, andK ALT NEW(Sig.m),andAR ALTITUDE 1,AR ALTITUDE 2, AR ALTITUDE 3, AR ALTITUDE 4,andAR ALTITUDE NEW(Sig. n), andtheAR STATUS 1,AR STATUS 2,AR STATUS 3,AR STATUS 4, and AR STATUS NEW (Sig. o) as wellas AR STATUS, AR ALTITUDE, and K ALT (Sigs. pr) are all defined the same as in case one. Predicate u, v,and w represent value ranges of the variables and predicatex defines the possible element values of the predefinedsets in Signature n as was true for case one.Predicate y requires that the updates to AR STATUS andK ALT occur when FRAME COUNTER? is odd and theradar echo pulse is received on time.Predicate z requires that the updates to AR STATUS andK ALT occur when FRAME COUNTER? is odd, the echoof the radar echo pulse has not yet been received, and all ofthe AR STATUS elements are healthy.The ARSP schema (Figure 7) is the main functionalschema of the ARSP module. The ARSP RESOURCE6

schema is imported (and is modified) in the Signature j.The Altitude Polynomial function (Sig. k) obtainsthe AR ALTITUDE

software unlike the IEEE Std 830-1998. The IEEE standard outlines the specific material and format needed. The GCS however has a concrete and systematic format that it uses to present its content. The format is resembles the old B5 style format used in various Military proje