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 Li
ary 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 li
ary 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 li
ary - containing only books – and
e able to perform the following tasks:
• Add a book
• Add a bo
owe
• Delete a book
• Delete a bo
owe
• Lend a book to a bo
owe
• Return a book from a bo
owe
• 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
lecture
tuto
CRICOS Provider No. 00103D ITECH7410 Assignment 2 - Group Page 3 of 3
Marking Criteria/Ru
ic
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/cu
ent-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 Li
ary System
Overview
Timelines and Expectations
Learning Outcomes Assessed
Assessment Details
Submission
Marking Criteria/Ru
ic
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: XXXXXXXXXXis 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
ackets (x1, x2, x3,…, xn)
To select one element can use the tuple selection operato
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
irthday: NAME DATE
known = dom birthday
*
The State Space for a Birthday Book
A possible state of the system…
known = { John, Mike, Susan }
irthday = { John 25-Mar-70,
Mike 20-Dec-60,
Susan 15-Apr-65 }
The state space for the implementation:
[NAME, DATE]
domain
ange
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
irthday’ = 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 pai
*
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 e
ors
ie pre-conditions are always true
What if e
ors occur?
Options:
Scrap the specification and start again
Add to the existing specification
Using the second approach:
Describe separately e
ors and responses to them
Use the Z schema calculus to combine specifications
*
Handling E
ors (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 E
ors (2)
*
Success
esult! : REPORT
esult! = 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
esult! : REPORT
name? known
esult! = already_known
Combining with AddBirthday …
*
AlreadyKnown Schema
RAddBirthday ( AddBirthday Success )
AlreadyKnown
Introduces a new schema ie “is defined as”
*
NotKnown
BirthdayBook
name? : NAME
esult! : REPORT
name? known
esult! = not_known
Robust version of FindBirthday …
*
NotKnown Schema
RFindBirthday ( FindBirthday Success )
NotKnown
*
*
Examples
Develop a formal