School of Engineering and Information Technology ITECH7410 - Software Engineering Methodologies Assignment 2, 2018/17 ...

1 answer below »


School of Engineering and Information Technology





ITECH7410 - Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________





Assignment 2 – Formal System Specification




Overview



The purpose of this assessment is to provide students with the opportunity to apply knowledge and skills developed during the semester with particular reference to the formal specification of a system through the use of Z notation. Students complete the assignment in groups of two.



As described in this course’s third study guide,
Software Analysis, Modelling and Specification, a Formal Specification (Technique) is one that has a rigorous mathematical basis and one of its advantages is that it can be mathematically checked for completeness. The course’s fourth study guide,
System and Software Design, also states that by using formal methods it is possible to derive a formal design from a formal specification and then be able to prove that the design and specification are functionally equivalent.



Your text,
Software Engineering: A Practitioners Approach
(Pressman, 2010) indicates that formal methods provide frameworks that allow people to specify, develop and verify systems in a structured and systematic way and that the mathematical based specification language used in formal methods ensures a greater chance of consistency, completeness and lack of ambiguity in a specification. Pressman also discusses formal specification languages and their common components – syntax, semantics and sets of relations. Of the four formal specification languages he identifies – OCL, LARCH, VDM and Z – he provides useful discussion with respect to OCL and Z.



In this assignment, you will use the Z specification language to provide the sets, relations and functions in schemas to specify the Container Control System (CCS) described below. Your schemas should provide the stored data that the system accesses and alters and identify the operations that are applied to change the state as well as the relationships that occur within the system. Remember, as specified in Spivey’s 2001 text,
The Z Notation: A
Reference Manual, schemas are utilized to illustrate both static and dynamic aspects of a system. Static aspects
include such things as the states a system occupies and the invariant relationships that continue to exist as the system moves between states. Dynamic aspects include the changes of state that occur, possible operations and the relationships between their inputs and outputs. Remember also you should always be conscious of the fact that a specification tries to describe what the system must do without saying how it is to be done (Spivey, 2001).



Keep all the above in mind as you read the following information. You are required to create a set of Z schema that adequately describes the CCS. Your assignment should include at least one state space and provide schema for the prescribed functions (including error handling) described below.








CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 1 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Timelines and Expectations



Marks:
Assignment will be assessed based on a mark out of 100



The following information is a summary from your Course Description:



Percentage Value of Task:
20% of the course marks



Due:
Week 12, Thursday 4:00pm



Minimum time expectation:
20 hours (per student)






Learning Outcomes Assessed




The following course learning outcomes are assessed by completing this assessment:




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



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





Requirements



Demonstrate an understanding of particular concepts covered in lectures, tutorials, laboratories and reading to provide the specification requested. This may require further reading and research beyond the material discussed in class.













CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 2 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Assessment Details



This assignment will be assessed by your lecturer/tutor. The assignment requires you to produce a formal specification containing the components identified below.




Background – Container Control System (CCS)



As a Software Engineering consultant, your task is to develop a formal specification in Z for the Container Control System (CCS). The CCS is a new computerized system to be developed for the storage and handling of accounts for freight companies and truck container deliveries/pickups to/from the Port of Melbourne (PoM) container terminals.



This system could be quite complicated. However, to simplify the system for this assignment only the following detail will be included in the proposed system (we do not for example track individual containers but only truck deliveries and pickups and ship loading and unloading and we assume one container size only (standard twenty-foot equivalent unit (TEU)):




Container Terminal



The PoM currently has four container terminals in Melbourne but the system must be written to seamlessly handle at least twice that number.



Each terminal has a unique name and storage capacity (in number of containers and tonnes) that must be stored in the proposed system.



The system must maintain the current tonnage and current number of containers in the container terminal.



When the container terminal is full no further deliveries of containers can be made to that container terminal and no unloading of containers from ships can occur before some are loaded onto a ship for shipping to their destination or some are picked up by trucks and taken away from the terminal.



Only five trucks can deliver into a particular container terminal at any one time and only five trucks can pick up containers from the container terminal at any one time. During busy times each container terminal maintains two queues of trucks - waiting to deliver and waiting to pick up.



Trucks wanting to deliver should only be entered into the waiting queue when there is sufficient room in the container terminal for all the container(s) that the truck holds i.e. the system needs to know that the current storage plus all the loads currently in the queue will not exceed the container terminal’s capacity tonnage or number of containers capacity.










CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 3 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________



For simplicity, we will say that a berth is always available for a ship to load or unload.



A container terminal cannot load more containers onto a ship than are currently stored at the terminal.



A container terminal cannot unload more containers from a ship than there is available space at the terminal.



When a container terminal is loading containers onto a ship, operational and safety considerations dictate that no trucks can deliver any containers to that container terminal (i.e. they must wait in the delivery queue).The system will ensure that all deliveries and pickups currently executing are completed before loading starts.



Similarly when a container terminal is unloading containers from a ship, operational and safety considerations dictate that no trucks can pick up any containers from that container terminal (i.e. they must wait in the pickup queue). The system will ensure that all deliveries and pickups currently executing are completed before unloading starts.




Trucks



The system maintains a list of registered trucks, their registration, owner and their empty weight (in tonnes).



As each loaded truck arrives at the container terminal, it is weighed to ascertain the weight of the containers on the truck. This is calculated as the difference between the weight of the loaded truck and its empty weight. The number of containers on the truck is also registered.



If there is sufficient room in the container terminal then the container(s) are placed in the container terminal and a record is kept of the number and tonnage delivered against both the truck registration number and the freight company providing the container(s).



When container(s) are placed on a truck to take them away from the terminal, the truck is weighed to ascertain the weight of the containers on the truck and the number of containers taken away is also recorded.




Freight Companies



The system will maintain a record of each freight company that assigns trucks to deliver containers to the container terminal and also each freight company that allocates trucks to pick up containers from the terminal.



Details to be kept include the freight company’s name, address and phone number.




Ships



The system will keep a record of all ships that have been registered to load or unload containers for the PoM.



The ship’s name, nationality (flag) and capacity (in number of containers and tonnes) will be stored.










CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 4 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________



The ship's captain can specify the number of containers and the tonnage to be loaded/unloaded onto/from the ship.



When loading a ship, the number of containers and tonnage to be loaded cannot be greater than the ships capacity and cannot be more than the available number of containers and tonnage in storage. The ship cannot load until all currently executing deliveries and pickups have completed (any new truck deliveries and pickups are placed in the appropriate queue). The system will keep a record of the number of containers and tonnage loaded onto the ship and adjust the remaining storage capacity in the container terminal and ship appropriately.



When unloading a ship, the number of containers and tonnage to be unloaded cannot be greater than the remaining storage capacity in the container terminal. The ship cannot unload until all currently executing deliveries and pickups have completed (any new truck deliveries and pickups are placed in the appropriate queue).The system will keep a record of the number of containers and tonnage unloaded from the ship and adjust the remaining storage capacity in the container terminal and ship appropriately.




Date and Time



Normally the date and time of each operation (truck delivery, truck pick up, ship loading, ship unloading) would be recorded. However to simplify this assignment those aspects will be ignored. Instead, a sequential count of each operation for each container terminal should be kept. Therefore, there should be a history of the order of truck delivery, ship loading, ship unloading and truck pickup operations that take place for each container terminal. There is also a need to keep track of the operation order between terminals. Therefore a global sequential number of the operations at terminals should be kept as well



The system would be able to say for example, that at container terminal SWANSON, count 999 involved the delivery of 2 containers of 3.5 (1.5 and 2.0) tonnes respectively by the truck registered AAA203 (owned by Gunner Myson) from freight company Freight’s Rates. The global operation 12337 at WEBB was a container pickup of 1 container weighing 2.0 tonnes by a truck with registration ABA713 and requested by the On The Way freight company. The next operation at SWANSON, with Global No of 12340 and Count of 1000 was a Pickup of 2 containers weighing 2.5 tonnes for the Container Carriers freight company. Global event number 12338 occured at VICTORIA and it was the un-loading of 2000 containers weighing 3500.0 tonnes from the Southern Star container ship and Global event number 12339 at APPLETON was the loading of the Liberian Princess container ship with 1500 containers weighing in total, 2000.0 tonnes. Sometime and some events later, Global event number 12500 at VICTORIA with a count of 650 was the loading of the Southern Star with 1200 containers at 2500.0 total tonnage.



The following table gives an example of this record of events:













CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 5 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________
































































































































































Global No



Container



Count



Operation



Vehicle



Qty



Tonnes



Freight





Terminal







Identifier







Company



12336



SWANSON



999



Delivery



AAA203



2



3.5



Freight’s

















Rates



12337



WEBB



555



Pickup



ABA713



1



2.0



On The

















Way



12338



VICTORIA



600



Un-Load



Southern Star



2000



3500.0





12339



APPLETON



750



Load



Liberian



1500



2000.0













Princess









12340



SWANSON



1000



Pickup



QWE810



2



2.5



Container

















Carriers



















12500



VICTORIA



650



Load



Southern Star



1200



2500.0





















...



















Assessable Tasks/Requirements



You are to create a set of Z schemas that adequately describes the CCS. It should include at least one state space and the following operations:



• An initialization operation called
Init.



• An operation
Enter_new_container_terminal
that an operator uses to enter the details of a new container terminal into the system. Assume the new container terminal is currently empty.



• An operation
Accept_delivery
that an operator uses to signal to the system to begin delivery (placing in the container terminal) of x quantity and y tonnes of containers from a truck. Note that the system must do a check to see if that storage capacity is available in the container terminal. If it is not then an error message must be output and no truck delivery occurs. Additional information needed by this routine is the truck registration and the freight company’s name. If successful, this operation stores all necessary details into the system for that delivery. If five trucks are already delivering then this new truck will be placed in a queue waiting for its turn to deliver.



• An operation
Accept_pickup
that an operator uses to signal to the system to begin pickup (placing on the truck) of x quantity and y tonnes of containers from the container terminal. Additional information needed by this routine is the truck registration and the freight company’s name. If successful, this operation stores all necessary details into the system for that pickup. If five trucks are already picking up then this new truck will









CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 6 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________



be placed in a queue waiting for its turn to pickup.



• An operation
Leave_delivery_queue. This operation is run by the system operator each time there is a delivery queue for a container terminal and the driver of a specified truck decides that the anticipated waiting time is too long and leaves the queue. The operation outputs to the operator the list of trucks in the queue after the specified truck is removed. If no trucks are left in the queue a reasonable error message should be produced.



• An operation
Unload_ship
that an operator uses to signal to the system to begin unloading (placing in the container terminal) of x quantity and y tonnes of containers from the ship. Note the system must check that all deliveries and pickups have stopped before unloading can commence. A suitable message must be output until this has been achieved. The system must also do a check to see if the quantity and tonnage storage capacity is available in the container terminal. If this check fails, then an error message must be output and no ship unloading occurs. (From an operational perspective, the operator may, after consultation, try the operation again with adjusted values to have a successful ‘partial’ unload but you do not need to be concerned with this as the functionality already described would accommodate this process). Additional information needed by this routine is the ship identifier. If successful, this operation stores all necessary details into the system for that unloading.



• An operation
Container_terminal_account
that outputs the total number and tonnage of containers delivered to a particular container terminal by ALL freight companies in a specified time period (in this simplified system, that is the total quantity and tonnes delivered between two specified global count values e.g. 10000 and 10500).



• An operation
Ships_total_account
that outputs the total number and tonnage that a particular ship has loaded from ALL container terminals in the total history of the system.



• An operation
Freight_company_account
that outputs the total number and tonnage of containers delivered to and the total number and tonnage picked up from ALL container terminals for each freight company between two specified global count values.



You should provide robust versions of each operation that are capable of handling any possible error conditions. For example, if the ship or truck is not correctly registered in the system an appropriate error message must be given.



You should also add a narrative to explain any schemas or logic that you have used. Authorship should be made clear. You might be asked to explain and answer questions about your work.











CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 7 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Additional Information




General Comments



The submission must be presented in a professional, clear and concise manner. If you need further system information please use your initiative and make reasonable and logical assumptions. Questions of a general nature (for example to clarify some part of the assignment requirements) can also be sent to the discussion forum but these should not in any way provide solutions or parts thereof.




Readings



The following resources will assist you with this assignment:



• Weeks 4 and 5 study materials and Section 4 of study guide three;




The Z Notation: A Reference Manual
(Spivey, 2001);



• Chapter 21, sections 21.5, 21.6 and 21.7 of Pressman (2010);



• Solutions for problem 2 of week 6 tutorial problems;



• The Z Resources section of your Moodle shell; and



• Introduction to Z Notation -
http://www.youtube.com/watch?v=qfEe9luJmVE


































CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 8 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Submission




One group member should submit an electronic copy of the CCS Formal Specification via Moodle. Partner students please refer to your course lecturer for submission instructions. Please refer to the
Course Description
for information regarding late assignments, extensions, special consideration, and plagiarism. A reminder all academic regulations can be accessed via the university’s website, see:
http://federation.edu.au/staff/governance/legal/feduni-legislation/feduni-statutes-and-regulations




Marking Criteria



Work will be assessed according to the following:



• Your CCS Formal Specification must complete the items detailed within the Assessable Tasks/Requirements section of this document.



• Your CCS Formal Specification should be presented as business or management style report which adheres to academic writing presentation standards. Where applicable, it must contain high quality academic presentation, expression and features as outlined in:



o Federation University’s



§

Assignment Layout and Appearance Guidelines;






§

General Guide to Writing and Study Skills
,






§

General Guide to Referencing;

and






o


Features of Academic Writing


(from
UEfAP.com)




















































































CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 9 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Marking Rubric






























































































































































































































































































































Student Name and






Marker










No
















Date
































Item




Description




Max. Marks




Student Mark












Global Variables



Correct declaration and initialisation




5














State Space Schema



Correct declaration and type for variables




5







Correct predicates
















Init
Operation



Correct initialisation of variables




5














Enter_new_container



Correct schema for entry, error and success




10






_terminal
Operation



Correct robust expression






















Accept_delivery



Correct schema for test of available room, successful




10





Operation



delivery, successful queueing and error









Correct robust expression
















Accept_pickup



Correct schema for successful pickup, successful




10





Operation



queueing and error







Correct robust expression






















Leave_delivery_queu



Correct schema for removal of truck, list of trucks in




10






e
Operation



queue and error









Correct robust expression
















Unload_ship



Correct schema for test of delivery and pickups stopped,




10





Operation



available room, successful unloading, updating of system









and error









Correct robust expression
















Container_terminal_



Correct declaration and type for variables




10






account
Operation



Correct predicates






















Ships_total_account



Correct schema for report and error (no ship in system)




10





Operation



Correct robust expression






















Freight_company_ac



Correct declaration and type for variables




10






count
Operation



Correct predicates






















Report



Adheres to guidelines given for assignment (Any




5







assumptions must be clearly stated and appropriate)




























CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 10 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________

































Total Mark






100














Course Mark






20














Comments:
























Feedback



Assessment marks will be made available in fdlMarks, Feedback to individual students will be provided via Moodle or as direct feedback during your tutorial 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.




Any support material must be compiled from reliable sources such as the academic resources in Federation University library which might include, but not be limited to: the main library collection, library databases and the BONUS+ collection as well as any reputable online resources (you should confirm this with your tutor).




References



Pressman, R.S. (2010).
Software Engineering: A Practitioners Approach
(7th
ed).
McGraw-Hill. ISBN: 978-007-126782-3



Spivey, J.M. (2001).
The Z Notation: A Reference Manual
(2nd
ed.). Oxford, England: Author.



http://spivey.oriel.ox.ac.uk/wiki2/files/zrm/zrm.pdf










CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 11 of 11



School of Engineering and Information Technology





ITECH7410 - Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________





Assignment 2 – Formal System Specification




Overview



The purpose of this assessment is to provide students with the opportunity to apply knowledge and skills developed during the semester with particular reference to the formal specification of a system through the use of Z notation. Students complete the assignment in groups of two.



As described in this course’s third study guide,
Software Analysis, Modelling and Specification, a Formal Specification (Technique) is one that has a rigorous mathematical basis and one of its advantages is that it can be mathematically checked for completeness. The course’s fourth study guide,
System and Software Design, also states that by using formal methods it is possible to derive a formal design from a formal specification and then be able to prove that the design and specification are functionally equivalent.



Your text,
Software Engineering: A Practitioners Approach
(Pressman, 2010) indicates that formal methods provide frameworks that allow people to specify, develop and verify systems in a structured and systematic way and that the mathematical based specification language used in formal methods ensures a greater chance of consistency, completeness and lack of ambiguity in a specification. Pressman also discusses formal specification languages and their common components – syntax, semantics and sets of relations. Of the four formal specification languages he identifies – OCL, LARCH, VDM and Z – he provides useful discussion with respect to OCL and Z.



In this assignment, you will use the Z specification language to provide the sets, relations and functions in schemas to specify the Container Control System (CCS) described below. Your schemas should provide the stored data that the system accesses and alters and identify the operations that are applied to change the state as well as the relationships that occur within the system. Remember, as specified in Spivey’s 2001 text,
The Z Notation: A
Reference Manual, schemas are utilized to illustrate both static and dynamic aspects of a system. Static aspects
include such things as the states a system occupies and the invariant relationships that continue to exist as the system moves between states. Dynamic aspects include the changes of state that occur, possible operations and the relationships between their inputs and outputs. Remember also you should always be conscious of the fact that a specification tries to describe what the system must do without saying how it is to be done (Spivey, 2001).



Keep all the above in mind as you read the following information. You are required to create a set of Z schema that adequately describes the CCS. Your assignment should include at least one state space and provide schema for the prescribed functions (including error handling) described below.








CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 1 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Timelines and Expectations



Marks:
Assignment will be assessed based on a mark out of 100



The following information is a summary from your Course Description:



Percentage Value of Task:
20% of the course marks



Due:
Week 12, Thursday 4:00pm



Minimum time expectation:
20 hours (per student)






Learning Outcomes Assessed




The following course learning outcomes are assessed by completing this assessment:




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



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





Requirements



Demonstrate an understanding of particular concepts covered in lectures, tutorials, laboratories and reading to provide the specification requested. This may require further reading and research beyond the material discussed in class.













CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 2 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Assessment Details



This assignment will be assessed by your lecturer/tutor. The assignment requires you to produce a formal specification containing the components identified below.




Background – Container Control System (CCS)



As a Software Engineering consultant, your task is to develop a formal specification in Z for the Container Control System (CCS). The CCS is a new computerized system to be developed for the storage and handling of accounts for freight companies and truck container deliveries/pickups to/from the Port of Melbourne (PoM) container terminals.



This system could be quite complicated. However, to simplify the system for this assignment only the following detail will be included in the proposed system (we do not for example track individual containers but only truck deliveries and pickups and ship loading and unloading and we assume one container size only (standard twenty-foot equivalent unit (TEU)):




Container Terminal



The PoM currently has four container terminals in Melbourne but the system must be written to seamlessly handle at least twice that number.



Each terminal has a unique name and storage capacity (in number of containers and tonnes) that must be stored in the proposed system.



The system must maintain the current tonnage and current number of containers in the container terminal.



When the container terminal is full no further deliveries of containers can be made to that container terminal and no unloading of containers from ships can occur before some are loaded onto a ship for shipping to their destination or some are picked up by trucks and taken away from the terminal.



Only five trucks can deliver into a particular container terminal at any one time and only five trucks can pick up containers from the container terminal at any one time. During busy times each container terminal maintains two queues of trucks - waiting to deliver and waiting to pick up.



Trucks wanting to deliver should only be entered into the waiting queue when there is sufficient room in the container terminal for all the container(s) that the truck holds i.e. the system needs to know that the current storage plus all the loads currently in the queue will not exceed the container terminal’s capacity tonnage or number of containers capacity.










CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 3 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________



For simplicity, we will say that a berth is always available for a ship to load or unload.



A container terminal cannot load more containers onto a ship than are currently stored at the terminal.



A container terminal cannot unload more containers from a ship than there is available space at the terminal.



When a container terminal is loading containers onto a ship, operational and safety considerations dictate that no trucks can deliver any containers to that container terminal (i.e. they must wait in the delivery queue).The system will ensure that all deliveries and pickups currently executing are completed before loading starts.



Similarly when a container terminal is unloading containers from a ship, operational and safety considerations dictate that no trucks can pick up any containers from that container terminal (i.e. they must wait in the pickup queue). The system will ensure that all deliveries and pickups currently executing are completed before unloading starts.




Trucks



The system maintains a list of registered trucks, their registration, owner and their empty weight (in tonnes).



As each loaded truck arrives at the container terminal, it is weighed to ascertain the weight of the containers on the truck. This is calculated as the difference between the weight of the loaded truck and its empty weight. The number of containers on the truck is also registered.



If there is sufficient room in the container terminal then the container(s) are placed in the container terminal and a record is kept of the number and tonnage delivered against both the truck registration number and the freight company providing the container(s).



When container(s) are placed on a truck to take them away from the terminal, the truck is weighed to ascertain the weight of the containers on the truck and the number of containers taken away is also recorded.




Freight Companies



The system will maintain a record of each freight company that assigns trucks to deliver containers to the container terminal and also each freight company that allocates trucks to pick up containers from the terminal.



Details to be kept include the freight company’s name, address and phone number.




Ships



The system will keep a record of all ships that have been registered to load or unload containers for the PoM.



The ship’s name, nationality (flag) and capacity (in number of containers and tonnes) will be stored.










CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 4 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________



The ship's captain can specify the number of containers and the tonnage to be loaded/unloaded onto/from the ship.



When loading a ship, the number of containers and tonnage to be loaded cannot be greater than the ships capacity and cannot be more than the available number of containers and tonnage in storage. The ship cannot load until all currently executing deliveries and pickups have completed (any new truck deliveries and pickups are placed in the appropriate queue). The system will keep a record of the number of containers and tonnage loaded onto the ship and adjust the remaining storage capacity in the container terminal and ship appropriately.



When unloading a ship, the number of containers and tonnage to be unloaded cannot be greater than the remaining storage capacity in the container terminal. The ship cannot unload until all currently executing deliveries and pickups have completed (any new truck deliveries and pickups are placed in the appropriate queue).The system will keep a record of the number of containers and tonnage unloaded from the ship and adjust the remaining storage capacity in the container terminal and ship appropriately.




Date and Time



Normally the date and time of each operation (truck delivery, truck pick up, ship loading, ship unloading) would be recorded. However to simplify this assignment those aspects will be ignored. Instead, a sequential count of each operation for each container terminal should be kept. Therefore, there should be a history of the order of truck delivery, ship loading, ship unloading and truck pickup operations that take place for each container terminal. There is also a need to keep track of the operation order between terminals. Therefore a global sequential number of the operations at terminals should be kept as well



The system would be able to say for example, that at container terminal SWANSON, count 999 involved the delivery of 2 containers of 3.5 (1.5 and 2.0) tonnes respectively by the truck registered AAA203 (owned by Gunner Myson) from freight company Freight’s Rates. The global operation 12337 at WEBB was a container pickup of 1 container weighing 2.0 tonnes by a truck with registration ABA713 and requested by the On The Way freight company. The next operation at SWANSON, with Global No of 12340 and Count of 1000 was a Pickup of 2 containers weighing 2.5 tonnes for the Container Carriers freight company. Global event number 12338 occured at VICTORIA and it was the un-loading of 2000 containers weighing 3500.0 tonnes from the Southern Star container ship and Global event number 12339 at APPLETON was the loading of the Liberian Princess container ship with 1500 containers weighing in total, 2000.0 tonnes. Sometime and some events later, Global event number 12500 at VICTORIA with a count of 650 was the loading of the Southern Star with 1200 containers at 2500.0 total tonnage.



The following table gives an example of this record of events:













CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 5 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________
































































































































































Global No



Container



Count



Operation



Vehicle



Qty



Tonnes



Freight





Terminal







Identifier







Company



12336



SWANSON



999



Delivery



AAA203



2



3.5



Freight’s

















Rates



12337



WEBB



555



Pickup



ABA713



1



2.0



On The

















Way



12338



VICTORIA



600



Un-Load



Southern Star



2000



3500.0





12339



APPLETON



750



Load



Liberian



1500



2000.0













Princess









12340



SWANSON



1000



Pickup



QWE810



2



2.5



Container

















Carriers



















12500



VICTORIA



650



Load



Southern Star



1200



2500.0





















...



















Assessable Tasks/Requirements



You are to create a set of Z schemas that adequately describes the CCS. It should include at least one state space and the following operations:



• An initialization operation called
Init.



• An operation
Enter_new_container_terminal
that an operator uses to enter the details of a new container terminal into the system. Assume the new container terminal is currently empty.



• An operation
Accept_delivery
that an operator uses to signal to the system to begin delivery (placing in the container terminal) of x quantity and y tonnes of containers from a truck. Note that the system must do a check to see if that storage capacity is available in the container terminal. If it is not then an error message must be output and no truck delivery occurs. Additional information needed by this routine is the truck registration and the freight company’s name. If successful, this operation stores all necessary details into the system for that delivery. If five trucks are already delivering then this new truck will be placed in a queue waiting for its turn to deliver.



• An operation
Accept_pickup
that an operator uses to signal to the system to begin pickup (placing on the truck) of x quantity and y tonnes of containers from the container terminal. Additional information needed by this routine is the truck registration and the freight company’s name. If successful, this operation stores all necessary details into the system for that pickup. If five trucks are already picking up then this new truck will









CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 6 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________



be placed in a queue waiting for its turn to pickup.



• An operation
Leave_delivery_queue. This operation is run by the system operator each time there is a delivery queue for a container terminal and the driver of a specified truck decides that the anticipated waiting time is too long and leaves the queue. The operation outputs to the operator the list of trucks in the queue after the specified truck is removed. If no trucks are left in the queue a reasonable error message should be produced.



• An operation
Unload_ship
that an operator uses to signal to the system to begin unloading (placing in the container terminal) of x quantity and y tonnes of containers from the ship. Note the system must check that all deliveries and pickups have stopped before unloading can commence. A suitable message must be output until this has been achieved. The system must also do a check to see if the quantity and tonnage storage capacity is available in the container terminal. If this check fails, then an error message must be output and no ship unloading occurs. (From an operational perspective, the operator may, after consultation, try the operation again with adjusted values to have a successful ‘partial’ unload but you do not need to be concerned with this as the functionality already described would accommodate this process). Additional information needed by this routine is the ship identifier. If successful, this operation stores all necessary details into the system for that unloading.



• An operation
Container_terminal_account
that outputs the total number and tonnage of containers delivered to a particular container terminal by ALL freight companies in a specified time period (in this simplified system, that is the total quantity and tonnes delivered between two specified global count values e.g. 10000 and 10500).



• An operation
Ships_total_account
that outputs the total number and tonnage that a particular ship has loaded from ALL container terminals in the total history of the system.



• An operation
Freight_company_account
that outputs the total number and tonnage of containers delivered to and the total number and tonnage picked up from ALL container terminals for each freight company between two specified global count values.



You should provide robust versions of each operation that are capable of handling any possible error conditions. For example, if the ship or truck is not correctly registered in the system an appropriate error message must be given.



You should also add a narrative to explain any schemas or logic that you have used. Authorship should be made clear. You might be asked to explain and answer questions about your work.











CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 7 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Additional Information




General Comments



The submission must be presented in a professional, clear and concise manner. If you need further system information please use your initiative and make reasonable and logical assumptions. Questions of a general nature (for example to clarify some part of the assignment requirements) can also be sent to the discussion forum but these should not in any way provide solutions or parts thereof.




Readings



The following resources will assist you with this assignment:



• Weeks 4 and 5 study materials and Section 4 of study guide three;




The Z Notation: A Reference Manual
(Spivey, 2001);



• Chapter 21, sections 21.5, 21.6 and 21.7 of Pressman (2010);



• Solutions for problem 2 of week 6 tutorial problems;



• The Z Resources section of your Moodle shell; and



• Introduction to Z Notation -
http://www.youtube.com/watch?v=qfEe9luJmVE


































CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 8 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Submission




One group member should submit an electronic copy of the CCS Formal Specification via Moodle. Partner students please refer to your course lecturer for submission instructions. Please refer to the
Course Description
for information regarding late assignments, extensions, special consideration, and plagiarism. A reminder all academic regulations can be accessed via the university’s website, see:
http://federation.edu.au/staff/governance/legal/feduni-legislation/feduni-statutes-and-regulations




Marking Criteria



Work will be assessed according to the following:



• Your CCS Formal Specification must complete the items detailed within the Assessable Tasks/Requirements section of this document.



• Your CCS Formal Specification should be presented as business or management style report which adheres to academic writing presentation standards. Where applicable, it must contain high quality academic presentation, expression and features as outlined in:



o Federation University’s



§

Assignment Layout and Appearance Guidelines;






§

General Guide to Writing and Study Skills
,






§

General Guide to Referencing;

and






o


Features of Academic Writing


(from
UEfAP.com)




















































































CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 9 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________




Marking Rubric






























































































































































































































































































































Student Name and






Marker










No
















Date
































Item




Description




Max. Marks




Student Mark












Global Variables



Correct declaration and initialisation




5














State Space Schema



Correct declaration and type for variables




5







Correct predicates
















Init
Operation



Correct initialisation of variables




5














Enter_new_container



Correct schema for entry, error and success




10






_terminal
Operation



Correct robust expression






















Accept_delivery



Correct schema for test of available room, successful




10





Operation



delivery, successful queueing and error









Correct robust expression
















Accept_pickup



Correct schema for successful pickup, successful




10





Operation



queueing and error







Correct robust expression






















Leave_delivery_queu



Correct schema for removal of truck, list of trucks in




10






e
Operation



queue and error









Correct robust expression
















Unload_ship



Correct schema for test of delivery and pickups stopped,




10





Operation



available room, successful unloading, updating of system









and error









Correct robust expression
















Container_terminal_



Correct declaration and type for variables




10






account
Operation



Correct predicates






















Ships_total_account



Correct schema for report and error (no ship in system)




10





Operation



Correct robust expression






















Freight_company_ac



Correct declaration and type for variables




10






count
Operation



Correct predicates






















Report



Adheres to guidelines given for assignment (Any




5







assumptions must be clearly stated and appropriate)




























CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 10 of 11





School of Engineering and Information Technology





ITECH7410 Software Engineering Methodologies Assignment 2, 2018/17



__________________________________________________________________________________

































Total Mark






100














Course Mark






20














Comments:
























Feedback



Assessment marks will be made available in fdlMarks, Feedback to individual students will be provided via Moodle or as direct feedback during your tutorial 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.




Any support material must be compiled from reliable sources such as the academic resources in Federation University library which might include, but not be limited to: the main library collection, library databases and the BONUS+ collection as well as any reputable online resources (you should confirm this with your tutor).




References



Pressman, R.S. (2010).
Software Engineering: A Practitioners Approach
(7th
ed).
McGraw-Hill. ISBN: 978-007-126782-3



Spivey, J.M. (2001).
The Z Notation: A Reference Manual
(2nd
ed.). Oxford, England: Author.



http://spivey.oriel.ox.ac.uk/wiki2/files/zrm/zrm.pdf










CRICOS Provider No. 00103D ITECH7410_Assignment2_sem9_2018_201817_T_Keogh Page 11 of 11

Answered Same DaySep 20, 2020ITECH7402

Answer To: School of Engineering and Information Technology ITECH7410 - Software Engineering Methodologies...

Meenakshi answered on Sep 27 2020
146 Votes
9/17/2018
(
[Type the company name]
[Year]
[Type the document title]
[Type the document subtitle]
admin
)
[endnoteRef:2]
Software Requirement for truck loading system for ship
Truck system TruckSystem members : P SHIP shelved : P LOADS checked : LOADS 7→ SHIP shelved ∩ dom checked = ∅ ran checked ⊆ memb
ers ∀ mem : SHIP • #(checked ✄ {mem }) ≤ MaxLoad
User-defined Types
individual ships [SHIP]
assume a given type: [TRUCK]
TRUCK == 1. . 59999
Output messages: MESSAGE :: = ‘OK’ | ‘Container already exists’ | ‘No such container’ | ‘Container has no registration’ | ‘Invalid register number’ | ‘Invalid entry’ | ‘Entry already exists’
Truck loading System
A set of type SHIP representing the container: container : P SHIP • Abstract representation of an instance of container:
: SHIP ↔ TRUCK
We can now define the before state and after state of Truckloading:
Before state
Accept_pickupcontainer : P SHIP system : SHIP ↔ TRUCK dom system ⊆ container
After state (decorate names with prime)
Accept_pickup′ container ′ : P SHIP system ′ : SHIP ↔ TRUCK dom system ′ ⊆ container ′
Defining ∆Accept_pickupSystem
• ∆Truckloading: ∆Accept_pickupcontainer,container ′ : P SHIP system, system ′ : SHIP ↔ TRUCK dom system ⊆ container dom system ′ ⊆ container ′ • Or alternatively as: ∆Accept_pickupAccept_pickupAccept_pickup′ Slide 57 Defining ΞAccept_pickupSystem • ΞTruckloading: ΞAccept_pickup∆Accept_pickupcontainer ′ = container system ′ = system
Defining the Initial State of Accept_pickupSystem
Presenting the initial state
InitAccept_pickup′ Accept_pickup′ container ′ = {} system ′ = {}
Adding a New Container to Accept_pickupSystem
Input to the operation: name? : SHIP • Output from the operation: rep! : MESSAGE • Successful operation: AddMemberOK ∆Accept_pickupname? : SHIP rep! : MESSAGE name ? 6∈ container container ′ = container ∪ {name ? } system ′ = system rep! = ‘OK’
Error Cases:
Container already exists in the Truckloading, i.e., name ? ∈ container ContainerExists ΞAccept_pickupname? : SHIP rep! : MESSAGE name ? ∈ container rep! = ‘Container already exists’
A total definition: AddMember =b AddMemberOK ∨ ContainerExists
Adding an Entry to Accept_pickupSystem
Input to the operation: name? : SHIP and register? : TRUCK • Output report from the operation: rep! : MESSAGE • Successful operation: AddEntryOK ∆Accept_pickupname? : SHIP register? : TRUCK rep! : MESSAGE name ? ∈ container name ? ֏ register ? 6∈ system system ′ = system ∪ {name ? ֏ register ? } container ′ = container rep! = ‘OK’
Error Cases: • Input not a legitimate container, i.e., name ? 6∈ container
Entry already exists in system, i.e., name ? ֏ register ? ∈ system EntryExists ΞAccept_pickupregister? : TRUCK name? : SHIP rep! : MESSAGE name ? ֏ register ? ∈ system rep! = ‘Entry already exists’
Constructing a total operation for adding an entry:
AddEntry =b AddEntryOK ∨ NotContainer ∨ EntryExists
Unload_ship a Container from Accept_pickupSystem
• Input: name? : SHIP • Output: rep!: MESSAGE • Successful operation: unloadContainerOK ∆Accept_pickupname? : SHIP rep! : MESSAGE name ? ∈ container...
SOLUTION.PDF

Answer To This Question Is Available To Download

Related Questions & Answers

More Questions »

Submit New Assignment

Copy and Paste Your Assignment Here