ginni
Guide to Project for Supervisors ITECH7410 Software Engineering Methodologies CRICOS Provider No. 00103D ITECH7410 Assignment 2 - Group Page 1 of 3 Assignment 2 – Group Formal Specification of a Library System Overview This assignment provides students with the opportunity to apply the knowledge and skills developed during the semester. Students work in small teams (3-4) for assignment 2, in which they complete a formal specification for a library system. Timelines and Expectations Due: Thursday May 30 @23:59 (week 11) Percentage Value of Task: 20% Minimum Time Expectation: more than 10 hours Students will design, implement and test a specification for a system and answering questions relating to the artifacts provided. Learning Outcomes Assessed The following course learning outcomes are assessed by completing this assessment: Skills: S1. Critically analyse and use complex decision making to research and determine the appropriate Software Engineering tools and methodologies to utilize in a given situation. S2. Apply professional communication skills to support and manage the engineering of a large software system. S3. Review, critically analyse and develop artefacts to define processes for quality assurance, risk management and communication in large software development projects. S4. Implement quality assurance activities in order to verify user requirements and validate design decisions. Application of knowledge and skills: A1. Analysis of a large system development problem to decide upon the best methodological approach. A2. Development of appropriate artefacts to support and manage the software engineering process such as change control and configuration management. CRICOS Provider No. 00103D ITECH7410 Assignment 2 - Group Page 2 of 3 Assessment Details 1. Students will need to develop schema that will model a library - containing only books – and be able to perform the following tasks: • Add a book • Add a borrower • Delete a book • Delete a borrower • Lend a book to a borrower • Return a book from a borrower • Enquire about a book • Reserve a book • Enquire about a reservation • Cancel a reservation • Buy a Book • Receive a Book • Report of Books on Loan 2. The schema must be consistent and be shown to work using examples 3. Schema need to be annotated so that the Z statements are clearly expressed in plain language 4. Write three (3) non-trivial predicate statements about your system; explain them and show that they are true Submission Submit your specification, via Moodle, as a Word document labelled in the following way: StudentID1_StudentID2 .docx Attach all files that are needed (the report plus up to 4 files) in order to mark this assignment by your lecturer/tutor CRICOS Provider No. 00103D ITECH7410 Assignment 2 - Group Page 3 of 3 Marking Criteria/Rubric Task Marks Statement of Completion (Abstract) – who did what 5 Functionality (10 items) 20 Annotation of Z statements in every schema 20 Demonstration that the system works and is consistent 15 Three (3) non-trivial predicate statements which are shown to be true 10 Report1 20 Presentation (at a suitable time). Each member presents and answers questions. 5-7 min in total. 10 TOTAL /100 Final Grade /20 Feedback Marks in fdlMarks, feedback to individual students via Moodle and feedback in class Plagiarism: Plagiarism is the presentation of the expressed thought or work of another person as though it is one's own without properly acknowledging that person. You must not allow other students to copy your work and must take care to safeguard against this happening. More information about the plagiarism policy and procedure for the university can be found at http://federation.edu.au/students/learning-and- study/online-help-with/plagiarism. 1 https://federation.edu.au/current-students/learning-and-study/online-help-with/guides-to-your-assessments http://federation.edu.au/students/learning-and-study/online-help-with/plagiarism http://federation.edu.au/students/learning-and-study/online-help-with/plagiarism Assignment 2 – Group Formal Specification of a Library System Overview Timelines and Expectations Learning Outcomes Assessed Assessment Details Submission Marking Criteria/Rubric Feedback Marks in fdlMarks, feedback to individual students via Moodle and feedback in class Plagiarism: GCO1832 - COMPUTER PROGRAMMING 1A Faculty of Science Commonwealth of Australia Copyright Act 1968 Notice for paragraph 135ZXA (a) of the Copyright Act 1968 Warning This Material has been reproduced and communicated to you by or on behalf of Federation University Australia under Part VB of the Copyright Act 1968 (the Act). The Material in this communication may be subject to copyright under the Act. Any further reproduction or communication of this material by you may be the subject of copyright protection under the Act. Do not remove this notice. ITECH7410 Software Methodologies Specification Using Z * * Name Declarations Predicates * Z Schemas Variable declarations of the form variable : type Give the properties of, and relationships between variables The basic representation of schemas in Z: * Data types Integers (-ve, 0 and +ve whole numbers - http://en.wikipedia.org/wiki/Integer) Natural Numbers (0 and +ve whole numbers - http://en.wikipedia.org/wiki/Natural_numbers) Positive Integers 1 (+ve whole numbers) Actually both are subsets of the basic integer type So x: is equivalent to {x:Z| x 0} and x: 1 is equivalent to {x:Z| x > 0} Can also declare ranges day:1 .. 7 is equivalent to { day: | day 1 day 7 } Note that Z does not include basic types such as Reals, Booleans and Characters * Types in Z * User Defined Types User can define any type they like [NAME, PHONE_NUMBER] So NAME is an abstract type which can hold a single one of all the possible names Must be defined before they are used By convention written in all capitals No need to actually declare internal elements or size Free Types FreeType ::= Element1 | Element2 | … | Elementn Used for defining enumerated types etc Each value must be a distinct literal (disjoint value) RESULT ::= OK | WARNING | ERROR DIGIT ::= ‘0’ | ‘1’ | ‘2’ | ‘3’ | ‘4’ | ‘5’ | ‘6’ | ‘7’ | ‘8’ | ‘9’ Equivalent to DIGIT == {‘0’ , ‘1’ , ‘2’ , ‘3’ , ‘4’ , ‘5’ , ‘6’ , ‘7’ , ‘8’ , ‘9’ } * Types in Z (2) * Cartesian Products NAME ADDRESS TEL_NO Is the set of all three-tuple subsets of NAME, ADDRESS, TEL_NO Tuples Tuple shown as elements separated by commas within round brackets (x1, x2, x3,…, xn) To select one element can use the tuple selection operator tuple.index Example t == (Ray Smith, Salisbury Lane, 26462) t.1 = Ray Smith t.2 = Salisbury Lane t.3 = 26462 * Types in Z (3) * We can define global variables by declaring axiomatic definitions declaration predicate Example range : 0 range range 10 Note that the predicate part is optional global_constant : TYPE eg range : * Global Variables * * Birthday Book Example This example is taken from Chapter 1 of http://spivey.oriel.ox.ac.uk/~mike/zrm/ It is a classic simple example that allows us to demonstrate the basic capabilities of the Z specification language without becoming overly detailed and difficult to understand. The author is Mike Spivey a very well respected researcher in the formal methods field and a member of the team that developed the Z language. * BirthdayBook known: NAME birthday: NAME DATE known = dom birthday * The State Space for a Birthday Book A possible state of the system… known = { John, Mike, Susan } birthday = { John 25-Mar-70, Mike 20-Dec-60, Susan 15-Apr-65 } The state space for the implementation: [NAME, DATE] domain range NB: Important to understand why we need the powerset in the declaration of known. The type of Known is NAME as it contains a set from the powerset of NAME at any one time. birthday is a function which returns the birthday of a given name. Also why the predicate is needed to maintain consistency between the two variables * AddBirthday BirthdayBook name? : NAME date? : DATE name? known birthday’ = birthday { name? date? } * AddBirthday Function x? is an input to the system = state of the system changes (greek Delta) So basically we are saying: - we want to use the BirthdayBook statespace already declared - the contents of BirthdayBook are allowed to be changed in this schema - we need two inputs from the user; the name and birthdate of the person - we check that the name is not already entered in the set of known names - then we use the union operator to add to the birthday function the new name and date pair * FindBirthday BirthdayBook name? : NAME date! : DATE name? known date! = birthday(name?) * FindBirthday Function = state of the system does NOT change ( = greek Xi) x! = is an output from the system * Remind BirthdayBook today? : DATE cards! : NAME cards! = {n:known | birthday(n)= today?} * Remind Function y is a member of the set { x: S |… x … } if (and only if) y is a member of S and the … y … is satisfied (condition is obtained by replacing x with y) * InitBirthdayBook BirthdayBook known = * Initialising the System ie known is empty … therefore the function birthday is also empty due to the original predicate in the state space schema * Previous specifications assume no errors ie pre-conditions are always true What if errors occur? Options: Scrap the specification and start again Add to the existing specification Using the second approach: Describe separately errors and responses to them Use the Z schema calculus to combine specifications * Handling Errors (1) * Add an extra output result of type REPORT where REPORT ::= ok|already_known|not_known So we are declaring a type called REPORT which may only have one of these three defined values For producing output ok, already_known, and not_known, we need to define the following three respective schemas: Success AlreadyKnown NotKnown * Handling Errors (2) * Success result! : REPORT result! = ok * Success Schema ie whenever the operation is successful (it always is in this case) we just need to output OK * AlreadyKnown BirthdayBook name? : NAME result! : REPORT name? known result! = already_known Combining with AddBirthday … * AlreadyKnown Schema RAddBirthday ( AddBirthday Success ) AlreadyKnown Introduces a new schema ie “is defined as” * NotKnown BirthdayBook name? : NAME result! : REPORT name? known result! = not_known Robust version of FindBirthday … * NotKnown Schema RFindBirthday ( FindBirthday Success ) NotKnown * * Examples Develop a formal