Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Name : Intake : Contact Details : SD3049 Formal Methods in Software Engineering

Name : Intake : Contact Details : SD3049 Formal Methods in Software Engineering First Edition 2011 ISBN Publish by FTMS Consultants (M) Sdn Bhd Kuala Lumpur, Malaysia www.ftmsglobal.com Printed in Kuala Lumpur by FTMS Consultants (M) Sdn Bhd All our rights reserved. No part of this publication may be reproduced, stored in a retrieval system or transmitted, in any form or by any means, electronic, mechanical, photocopying, recording or otherwise, without the prior written permission of FTMS Consultants (M) Sdn Bhd. We are grateful to the academic members and module experts for permission to produce the syllabus, teaching guide and study materials of which contribute to FTMS. © FTMS Consultants (M) Sdn Bhd 2011 Contents Page 1. OVERVIEW ........................................................................................................................................... 4 2. INTRODUCTION TO FORMAL METHODS ................................................................................... 5 3. PROPOSITION .................................................................................................................................... 11 4. PROPOSITION EXERCISE ............................................................................................................... 15 5. PREDICATES ...................................................................................................................................... 17 6. PREDICATES EXERCISE ................................................................................................................. 21 7. SETS ...................................................................................................................................................... 23 8. SETS EXERCISE ................................................................................................................................. 29 9. SERIES OR SEQUENCE .................................................................................................................... 31 10. SERIES OR SEQUENCE EXERCISE .............................................................................................. 36 11. MATHEMATICAL PROOF ............................................................................................................... 38 12. TESTING .............................................................................................................................................. 41 13. APPLICATION TO FORMAL SPECIFICATION .......................................................................... 48 14. Z NOTATION ...................................................................................................................................... 52 15. REVISION ............................................................................................................................................ 61 16. REFERENCE: ...................................................................................................................................... 64 Overview Overview Overview Normally UEL subject taught in FTMS KL do not have any guide books, thus the reason in 2011, Mr. Trevor wishes to have guide books for UEL students on UEL subjects. As such this exercise will be carry out term by term and the lecturers teaching the given subjects will need to update their respective guide book for that given term. And if all goes well by the end of the year all the books in FTMS will have been updated including UEL. Thus I, Sola Lee was allocated this subject Network Programming as I have been teaching this subject for two (2) terms now. SD3049 is a 3rd year subject and student have a prerequisite of SD2054 (Software Development) which in turn require SD1042 (Introduction to Software Development). From my experience in teaching this subject, the student also needs to have a prerequisite of IM2042 (Information System Modeling and Design) which in turn require IM1045 (Information Systems). This is because Formal Methods main object is to scrutinize specification and design made before coding. The topics will initially revise basic mathematical concept like proposition, predicates, sets, series or sequences and mathematical proofs. Then the guide will use the above chapters and show how specification can be scrutinized using the above (especially during testing) to uncover potential omissions. Then finally the guide book will end with Z notation which is a formal language. Notice that for the basic mathematics concepts there will be a exercise classes to give the lecturers and the student time to try out and show their competency. -> Chapter 1- Formal Methods 5/64 Chapter 01 Introduction to Formal Methods 1. SDLC 2. Formal Method 3. Advantage 4. Disadvantage 5. Critical Software 6. Integrity Level 7. Stages in Formal Methods Chapter 1- Formal Methods 6/64 Revise Software Development When creating a software there are few engineering stages that is normally be followed to ensure that they software is built within the time and budget. These stages collectively are called the software development life cycle (SDLC). The SDLC can be divided into seven (7) stages; 1. Initial Study This is the first time the system development team meets the clients to collective information regarding the problem. Normally this stage delivers the proposal and quotation to the clients. 2. Analysis After the client has agreed to the proposal and price, the team will go in and study the current system with the intention to discover the source of the problem. The System analyst will use diagrams and data collection techniques (observation, inspections, interview, etc) to aid them. Normally this stage delivers a report stating the source of the problem and more then one alternative solutions. 3. Design After the client agrees with the analysis findings, the client will choose one (1) solution. From this one solution the system designer will create the specification. Take note that different IT section will require different specification. For the software section, the deliverables will take the form of a screen design, logic design, representation of the codes, etc. 4. Development Base on the given specification, the respective IT section will develop the solution. For the software section, the deliverables will be a full running software program created from the specification. 5. Testing The test documents (Test Plan and Test Case) are normally created by the System Analyst during the development stages. The tester (normally a 3rd party) will use the Test Plan and Test Case to complete the testing. The deliverables will be a letter from the tester stating the outcome of the test. Chapter 1- Formal Methods 7/64 6. Implementation At this stage onward the software is no longer a concern, the main objective now will be to prepare the environment. The implementation plan will list the tasks necessary to prepare the environment to accept new software, such as installation, training, conversion of data, change over method, etc. There are many deliverables here depending on what is listed in the implantation plan. For example for user training a user manual is normally created. 7. Review This is the final stage where the software user and team will sit down to review the software performance and to decide negotiate on the maintenance contract. If all goes well normally but not necessary a sign off letter will be the last deliverables. Formal Method Formal method is a way to takes the specification (written in natural language) and converts it into its mathematical equivalent. Thus it is normally used in the SDLC Analysis and Design stages. The natural language usually contains ambiguous, incomplete and inconsistent statement. Once a specification in English for example is translated to a mathematical form, it will remove all ambiguity and uncertainty in that statement. Formal method will also bring to light all different probable perspective to any given variables and functions that could have been hidden behind the English language. This can be done using a number of formal languages such as Z notation, VDM, Algebra, Functional Programming, etc. Creating software need not use formal method, having said that, having formal method imbedded into the SDLC does give the software huge advantages and also a new set of disadvantages Advantage of formal method Formal Method forces the System Analyst and Designer to think carefully about the specification as it enforce proper engineering approach using discrete mathematics. Formal Method forces the System Analyst and Designer to see all the different possible states for any given variables and functions thus will avoid many faults and therefore reduces the bugs and errors from the design stage onward. Chapter 1- Formal Methods 8/64 Disadvantage of formal method Formal Method requires the person to know how to apply discrete mathematics. It will obviously slow down the analysis and design stage resources and time therefore also the cost of the project. There are too many different formal methods and most of them are not compatible with each other. Formal methods do not guarantee that a specification is complete. For each variable and function, it just forces the System Analyst and Designer to view the specification from a different perspectives but it does not guarantee that variable and functions will not be left out. Critical software Having known the advantages and disadvantages, most clients will see the justification to use formal methods for critical systems, but this thinking is now slowly fading as most clients realize the important and cost saving and convenience of having a good specification initially in the SDLC. There are basically three (3) different types of critical systems; 1. Business Critical System Business Critical System refers to a system where the honesty and integrity of the business is paramount. All data kept in the system must be accurate at all times. If a fault is found the entire process must be stop to allow correction. Most government, business and manufacturing company that requires payment are business critical. 2. Mission Critical System Mission Critical System refers to a system where the continuous running of the system is paramount. Accurate takes a lower priority compare to the running of the system. Auto Teller Machine, Car ticketing system, Alarm Systems are mission critical. 3. Safety Critical System Safety Critical System refers to a system where the safety of everyone directly or indirectly affected by the system is paramount. Functionality and Accurate takes a lower priority compare to the safety of the users. Most medical, construction and oil rig systems are safety critical system. Many organizations today require a combination of the above as such you may have a business mission critical system, a business safety critical system, etc. Chapter 1- Formal Methods 9/64 Integrity Level Integrity level refers to how much cost is an organization is willing to spend and how much risk is an organization is willing to take when developing software. Integrity Level Cost Risk Example uploads/Litterature/ sd3049-formal-methods-in-software-engineering-name-intake-contact-details.pdf