CS 501: Software EngineeringCourse AdministrationPlanning for the PresentationSlide 4Formal SpecificationRememberFormal Specification using Mathematical NotationFormal Specification Using DiagramsFormal Specification of Programming LanguagesFormal Specification using Z ("Zed")Example: Specification using ZExample: Implementation of intrtExample: Program for intrtFormal Specification of Finite State Machine Using ZState Transition DiagramState Transition TableZ SpecificationZ Specification (continued)SchemasZ in PracticeUser Interface Design: Requirements and RefinementThe Design/Evaluate LoopPowerPoint PresentationMethods for Specifying Usability Requirements and Evaluation of UsabilityFocus GroupSpecial Considerations: DisabilitiesSpecial Considerations: Computer Systems and NetworksSpecial Considerations: Design Tensions in Networked SystemsSpecial Considerations: Device-Aware User InterfacesSpecial Considerations: Usability and Cost1CS 501 Spring 2006CS 501: Software EngineeringLecture 10Requirements 42CS 501 Spring 2006Course AdministrationPresentations, March 7-9Read the instructions on the Assignments Web page.Reserve a time slot by sending email to [email protected]. Time slots are listed on the home page of the Web site. First-come-first-served.Quiz 3This quiz may be moved to March 16.3CS 501 Spring 2006Planning for the PresentationHow will you use the time?This is a presentation to the client, with the Instructor as a secondary audience. Possible topics:• Overview of project and progress against plan• Presentation of assumptions, decisions• Summary of requirements in moderate detail• What has been learned since feasibility study. Changes in plansAllow 15 minutes for questions. Expect interruptions."This is our understanding of your requirements."4CS 501 Spring 2006Planning for the PresentationLogisticsHave a rehearsal, check visual aids and demonstrations. Then change nothing.Check out the equipment in the meeting room. What network will you use (if any). How will you connect a computer (if you do)? What about firewalls?Will one person act as chair and call on other members of the team? Never interrupt your colleagues. Not everybody is a great presenter, but everybody can be well-prepared.5CS 501 Spring 2006Formal SpecificationWhy?• Precise standard to define and validate software.Why not?• May be time consuming• Methods are not suitable for all applications6CS 501 Spring 2006RememberFormal specification does not prescribe the implementationWith formal specification it is possible, at least theoretically, to generate code automatically from the specification, but this may not be the most effective way:• Writing the generator may be a very large programming task.• The resulting code may perform badly.Formal specification does not guarantee correctness• If the specification is wrong, the system will be wrong.7CS 501 Spring 2006Formal Specification using Mathematical NotationMathematical requirements can be specified formally.Example: requirements from a mathematical package:B1, B2, ... Bk is a sequence of m x m matrices1, 2, ... k is a sequence of m x m elementary matrices B1-1 = 1B2-1 = 21Bk-1 = k ... 21The numerical accuracy must be such that, for all k, BkBk-1 - I < 8CS 501 Spring 2006Formal Specification Using Diagramsdigitunsigned integerdigit.E+-unsigned integerunsigned integerunsigned numberExample: Pascal number syntax9CS 501 Spring 2006Formal Specification of Programming Languages<unsigned number> ::= <unsigned integer> | <unsigned real><unsigned integer> ::= <digit> {<digit>}<unsigned real> ::= <unsigned integer> . <digit> {<digit>} | <unsigned integer> . <digit> {<digit>} E <scale factor> | <unsigned integer> E <scale factor><scale factor> ::= <unsigned integer> | <sign> <unsigned integer><sign> ::= + | -Example: Pascal number syntax10CS 501 Spring 2006Formal Specification using Z ("Zed")Z is a specification language developed by the Programming Research Group at Oxford University around 1980. Z is used for describing and modeling computing systems. It is based on axiomatic set theory and first order predicate logic.Ben Potter, Jane Sinclair, David Till,An Introduction to Formal Specification and Z(Prentice Hall) 1991Jonathan JackyThe Way of Z(Cambridge University Press) 199711CS 501 Spring 2006Informal: The function intrt(a) returns the largest integer whose square is less than or equal to a.Formal (Z):intrt: N N a : N • intrt(a) * intrt(a) < a < (intrt(a) + 1) * (intrt(a) + 1)Example: Specification using Z12CS 501 Spring 2006Example: Implementation of intrt 1 + 3 + 5 + ... (2n - 1) = n2Static specification does not describe the design of the system.A possible algorithm uses the mathematical identity:13CS 501 Spring 2006Example: Program for intrtint intrt (int a)/* Calculate integer square root */{ int i, term, sum; term = 1; sum = 1; for (i = 0; sum <= a; i++) { term = term + 2; sum = sum + term; } return i;}14CS 501 Spring 2006Formal Specification of Finite State Machine Using ZA finite state machine is a broadly used method of formal specification:• Event driven systems (e.g., games)• User interfaces• Protocol specificationetc., etc., ...15CS 501 Spring 2006State Transition DiagramPatientsFieldsSetup ReadyBeamonEnter EnterStartStopSelect fieldSelect patient(lock on)(lock off)16CS 501 Spring 2006State Transition TableSelectPatientSelectFieldEnterlock offStart Stoplock onPatientsFieldsSetupReadyBeamonFieldsFieldsFieldsPatientsPatientsPatientsSetupSetupSetupReadyBeamonReady17CS 501 Spring 2006Z SpecificationSTATE ::= patients | fields | setup | ready | beam_onEVENT ::= select_patient | select_field | enter | start | stop | lock_off | lock_onFSM == (STATE X EVENT) STATE no_change, transitions, control : FSMContinued on next slide18CS 501 Spring 2006Z Specification (continued)control = no_change transitionsno_change = { s : STATE; e : EVENT • (s, e) s }transitions = { (patients, enter) fields, (fields, select_patient) patients, (fields, enter) setup, (setup, select_patient) patients, (setup, select_field) fields, (setup, lock_off) ready, (ready, select_patient) patients, (ready, select_field) fields, (ready, start) beam_on, (ready, lock_on) setup, (beam_on, stop) ready,
View Full Document
Unlocking...