27 Formal Specification Systems Software And Technology-Books Pdf

27 Formal Specification Systems software and technology
30 Dec 2019 | 52 views | 0 downloads | 23 Pages | 363.51 KB

Share Pdf : 27 Formal Specification Systems Software And Technology

Download and Preview : 27 Formal Specification Systems Software And Technology


Report CopyRight/DMCA Form For : 27 Formal Specification Systems Software And Technology



Transcription

Chapter 27 Formal Specification 2, In traditional engineering disciplines such as electrical and civil engineering. progress has usually involved the development of better mathematical techniques. The engineering industry has had no difficulty accepting the need for mathematical. analysis and in incorporating mathematical analysis into its processes. Mathematical analysis is a routine part of the process of developing and validating. a product design, However software engineering has not followed the same path Although. there has now been more than 30 years of research into the use of mathematical. techniques in the software process these techniques have had a limited impact So. called formal methods of software development are not widely used in industrial. software development Most software development companies do not consider it. cost effective to apply them in their software development processes. The term formal methods is used to refer to any activities that rely on. mathematical representations of software including formal system specification. specification analysis and proof transformational development and program. verification All of these activities are dependent on a formal specification of the. software A formal software specification is a specification expressed in a language. whose vocabulary syntax and semantics are formally defined This need for a. formal definition means that the specification languages must be based on. mathematical concepts whose properties are well understood The branch of. mathematics used is discrete mathematics and the mathematical concepts are drawn. from set theory logic and algebra, In the 1980s many software engineering researchers proposed that using. formal development methods was the best way to improve software quality They. argued that the rigour and detailed analysis that are an essential part of formal. methods would lead to programs with fewer errors and which were more suited to. users needs They predicted that by the 21st century a large proportion of. software would be developed using formal methods, Clearly this prediction has not come true There are four main reasons for. 1 Successful software engineering The use of other software engineering. methods such as structured methods configuration management and. information hiding in software design and development processes have. resulted in improvements in software quality People who suggested that the. only way to improve software quality was by using formal methods were. clearly wrong, 2 Market changes In the 1980s software quality was seen as the key software.
engineering problem However since then the critical issue for many. classes of software development is not quality but time to market Software. must be developed quickly and customers are sometimes willing to accept. software with some faults if rapid delivery can be achieved Techniques for. rapid software development do not work effectively with formal. specifications Of course quality is still an important factor but it must be. achieved in the context of rapid delivery, Ian Sommerville 2009. 3 Chapter 27 Formal Specification, 3 Limited scope of formal methods Formal methods are not well suited to. specifying user interfaces and user interaction The user interface. component has become a greater and greater part of most systems so you. can only really use formal methods when developing the other parts of the. 4 Limited scalability of formal methods Formal methods still do not scale up. well Successful projects that have used these techniques have mostly been. concerned with relatively small critical kernel systems As systems increase. in size the time and effort required to develop a formal specification grows. disproportionately, These factors mean that most software development companies have been. unwilling to risk using formal methods in their development process However. formal specification is an excellent way of discovering specification errors and. presenting the system specification in an unambiguous way Organizations that. have made the investment in formal methods have reported fewer errors in the. delivered software without an increase in development costs It seems that formal. methods can be cost effective if their use is limited to core parts of the system and. if companies are willing to make the high initial investment in this technology. The use of formal methods is increasing in the area of critical systems. development where emergent system properties such as safety reliability and. security are very important The high cost of failure in these systems means that. companies are willing to accept the high introductory costs of formal methods to. ensure that their software is as dependable as possible As I discuss in Chapter 24. critical systems have very high validation costs and the costs of system failure are. large and increasing Formal methods can reduce these costs. Critical systems where formal methods have been applied successfully. include an air traffic control information system Hall 1996 railway signalling. systems Dehbonei and Mejia 1995 spacecraft systems Easterbrook et al 1998. and medical control systems Jacky 1995 Jacky et al 1997 They have also been. used for software tool specification Neil et al 1998 the specification of part of. IBM s CICS system Wordsworth 1991 and a real time system kernel Spivey. 1990 The Cleanroom method of software development Prowell et al 1999. relies on formally based arguments that code conforms to its specification Because. reasoning about the security of a system is also possible if a formal specification is. developed it is likely that secure systems will be an important area for formal. methods use Hall and Chapman 2002, 27 1 Formal specification in the software process. Critical systems development usually involves a plan based software process that is. based on the waterfall model of development discussed in Chapter 4 Both the. system requirements and the system design are expressed in detail and carefully. analysed and checked before implementation begins If a formal specification of. Ian Sommerville 2009, Chapter 27 Formal Specification 4.
Increasing contractor involvement, Decreasing client involvement. User System, Architectural Formal High level, requirements requirements. design specification design, definition specification. Figure 27 1, Specification Specification, and design. the software is developed this usually comes after the system requirements have. been specified but before the detailed system design There is a tight feedback loop. between the detailed requirements specification and the formal specification As I. discuss later one of the main benefits of formal specification is its ability to. uncover problems and ambiguities in the system requirements. The involvement of the client decreases and the involvement of the. contractor increases as more detail is added to the system specification In the early. stages of the process the specification should be customer oriented You should. write the specification so that the client can understand it and you should make as. few assumptions as possible about the software design However the final stage of. the process which is the construction of a complete consistent and precise. specification is principally intended for the software contractor It precisely. specifies the details of the system implementation You may use a formal language. at this stage to avoid ambiguity in the software specification. Figure 27 1 shows the stages of software specification and its interface with. the design process The specification stages shown in Figure 27 1 are not. independent nor are they necessarily developed in the sequence shown Figure 27 2. shows specification and design activities may be carried out in parallel streams. There is a two way relationship between each stage in the process Information is. fed from the specification to the design process and vice versa. As you develop the specification in detail your understanding of that. specification increases Creating a formal specification forces you to make a. detailed systems analysis that usually reveals errors and inconsistencies in the. informal requirements specification This error detection is probably the most. requirements, specification, specification, High level.
requirements, definition, Figure 27 2, specification in the. System Architectural, software process modelling design. Ian Sommerville 2009, 5 Chapter 27 Formal Specification. Validation, Design and, implementation Validation, Design and. implementation, Specification, Specification, Figure 27 3.
development costs, with formal, specification, potent argument for developing a formal specification Hall 1990 It helps you. discover requirements problems that can be very expensive to correct later. Depending on the process used specification problems discovered during. formal analysis might influence changes to the requirements specification if this. has not already been agreed If the requirements specification has been agreed and. is included in the system development contract you should raise the problems that. you have found with the customer It is then up to the customer to decide how they. should be resolved before you start the system design process. Developing and analysing a formal specification front loads software. development costs Figure 27 3 shows how software process costs are likely to be. affected by the use of formal specification When a conventional process is used. validation costs are about 50 of development costs and implementation and. design costs are about twice the costs of specification With formal specification. specification and implementation costs are comparable and system validation costs. are significantly reduced As the development of the formal specification uncovers. requirements problems rework to correct these problems after the system has been. designed is avoided, Two fundamental approaches to formal specification have been used to. write detailed specifications for industrial software systems These are. 1 An algebraic approach where the system is described in terms of operations. and their relationships, 2 A model based approach where a model of the system is built using. mathematical constructs such as sets and sequences and the system. operations are defined by how they modify the system state. Different languages in these families have been developed to specify. sequential and concurrent systems Figure 27 4 shows examples of the languages in. Ian Sommerville 2009, Chapter 27 Formal Specification 6. Sequential Concurrent, Algebraic Larch Guttag et al 1993 Lotos Bolognesi and Brinksma.
OBJ Futatsugi et al 1985 1987, Model based Z Spivey 1992 CSP Hoare 1985. Figure 27 4, Formal VDM Jones 1980 Petri Nets Peterson 1981. specification B Wordsworth 1996, each of these classes You can see from this table that most of these languages were. developed in the 1980s It takes several years to refine a formal specification. language so most formal specification research is now based on these languages. and is not concerned with inventing new notations, In this chapter my aim is to introduce both algebraic and model based. approaches The examples here should give you an idea of how formal. specification results in a precise detailed specification but I don t discuss. specification language details specification techniques or methods of program. verification You can download a more detailed description of both algebraic and. model based techniques from the book s website, 27 2 Sub system interface specification.
Large systems are usually decomposed into sub systems that are developed. independently Sub systems make use of other sub systems so an essential part of. the specification process is to define sub system interfaces Once the interfaces are. agreed and defined the sub systems can be developed independently. Sub system interfaces are often defined as a set of objects or components. Figure 27 5 These describe the data and operations that can be accessed through. the sub system interface You can therefore define a sub system interface. specification by combining the specifications of the objects that make up the. Precise sub system interface specifications are important because sub. system developers must write code that uses the services of other sub systems. Sub system Sub system, Figure 27 5 A B, Sub system. Ian Sommerville 2009, 7 Chapter 27 Formal Specification. SPECIFICATION NAME, imports LIST OF SPECIFICATION NAMES. Informal description of the sort and its operations. Figure 27 6 The Operation signatures setting out the names and the types of. structure of an the parameters to the operations defined over the sort. specification Axioms defining the operations over the sort. before these have been implemented The interface specification provides. information for sub system developers so that they know what services will be. available in other sub systems and how these can be accessed Clear and. unambiguous sub system interface specifications reduce the chances of. misunderstandings between a sub system providing some service and the sub. systems using that service, The algebraic approach was originally designed for the definition of abstract. reasoning about the security of a system is also possible if a formal specification is developed it is likely that secure systems will be an important area for formal methods use Hall and Chapman 2002 27 1 Formal specification in the software process Critical systems development usually involves a plan based software process that is

Related Books

ELECTRIC SEWING MACHINE 15 90

ELECTRIC SEWING MACHINE 15 90

SINGER ELECTRIC SEWING MACHINE 15 90 REVERSIBLE FEED LOCK STITCH FOR FAMILY USE When Reqmring Parts or Repairs for Yo r MachiBe Look for the Red S There are Singer Shops in Every City THE SINGER MANUFACTURING CO PRINTED IN U 8 A THE IMPORTANCE OF USING SINGER LUBRICANTS FOR YOUR ELECTRIC SEWING MACHINE The Best is the Cheapest Use SINGER Oil on Machine Knowing from many years

SINGER tinyinc files wordpress com

SINGER tinyinc files wordpress com

SINGER SERVICE Wherever you go xou will find expert dependable SINGER Service close at hand SINGER is interested in hdping you keep your SINGER Sewing Machine in top runuiig condition That is why you should alwaxs cail your SINGER SEWING CENIRE if your machine ever requires adjust ment or repair WhPIi You call your SINGER SEWING CENTRE you

Instruction Manual 4411 singer com

Instruction Manual 4411 singer com

Read all instructions before using this sewing machine 1 An appliance should never be left unattended when plugged in 2 Always unplug this appliance from the electric outlet immediately after using and before cleaning 3 Replace bulb with same type rated 15 watts 1 Do not allow to be used as a toy Close attention is necessary when this appliance is used by or near children 2 Use

M1500 M1505 Instruction Manual M1600 M1605

M1500 M1505 Instruction Manual M1600 M1605

A sewing machine should never be left unattended when plugged in The electrical socket to which the machine is plugged in should be easily accessible Always unplug this sewing machine from the electric outlet immediately after using and before cleaning removing covers lubricating or when making any other user servicing adjustments mentioned in the instruction manual WARNING To reduce

Instruction Manual 3321 singer com

Instruction Manual 3321 singer com

service center for examination repair electrical or mechanical adjustment 4 Never operate the appliance with any air openings blocked Keep ventilation openings of the sewing machine and foot controller free from accumulation of lint dust and loose cloth 5 Keep fingers away from all moving parts Special care is required around the sewing machine needle 6 Always use the proper needle

cover page IBM

cover page IBM

This SINGER sewing machine model 14T968DC IMPORTANT SAFETY INSTRUCTIONS When using this machine basic safety precautions should always be followed including the following Read all instructions before using the machine The machine should never be left unattended when plugged in Always unplug the machine from the electric outlet immediately after using and before cleaning Always

Einfach entspannt zur cklehnen Mercedes Benz sterreich

Einfach entspannt zur cklehnen Mercedes Benz sterreich

Preise f r Mercedes Benz Pkw CL G Klasse GL GLE GLS M Klasse S Klasse SL SLS und AMG Fahrzeuge Medieninhaber Mercedes Benz sterreich GmbH Mercedes Benz Platz 1 5301 Eugendorf Druck Samson Druck St Margarethen

MBO Archiv Mercedes Benz Offroad Mercedes Benz Driving

MBO Archiv Mercedes Benz Offroad Mercedes Benz Driving

neue G ganz der alte Lo gisch Die Karosserie hat sich seit 1979 nur maginal zum damaligen Baumuster 460 ver ndert und was an neuer Technik und zus tzlichem Komfort dazu kam bleibt weitestgehend im Verborge nen Uniformen unterliegen eben keinem Modediktat Da der einst als Milit r Gel nde wagen konzipierte G inzwischen en

Innovationskraft im Einsatz Mercedes Benz

Innovationskraft im Einsatz Mercedes Benz

Mercedes Benz Custom Tailored Trucks Die beste Adresse f r Umbauten an einem Mercedes Benz LKW ist Mercedes Benz selbst Bei Mercedes Benz Custom Tailored Trucks nutzen Spezialisten ihre jahrzehntelange Erfahrung im LKW Bau und finden passgenaue Antworten auf jeden Kundenwunsch Der Konstruktion geht eine genaue Analyse der Kundenbed rfnisse voraus Gemeinsam mit dem Kunden wird die beste

KOM Gesamtbestand Stand 01 11 2012 inkl Alter Wagen

KOM Gesamtbestand Stand 01 11 2012 inkl Alter Wagen

KOM Gesamtbestand Stand 01 11 2012 inkl Alter Wagen O 405 NK 1184 184 224 96 26 2 500 3 000 10 500 X Stadtbus Wiesloch Stadtbus Lackierung Evo Bus O 405 NK 1340 340 225 97 26 2 500 3 000 10 500 X Stadtbus Wiesloch Stadtbus Lackierung Evo Bus O 405 NK OG RB 1018 018 44 2 500 3 000 11 850 SWEG Mercedes Benz O 405 OG RB 1021 021 44 2 500 3 000 11 850 Schl sselbus Offenburg Stadtbus

mercedes benz WordPress com

mercedes benz WordPress com

Mercedes Benz F 600 HYGENIUS compact fuel cell car unveiled in 2005 Tokyo Motor Show Mercedes Benz Bionic Car unveiled in 2005 DaimlerChrysler Innovation Symposium in Washington modeled after boxfish Mercedes Benz Ocean Drive a 4 door convertible based on the S600 Mercedes Benz F700 Large luxury saloon featuring the small capacity high output DiesOtto engine