Developing Formal Specifications In Z
Developing Formal Specifications in ZHossein Saiedian, Ph.D.Electrical Engineering & Computer ScienceUniversity of Kansassaiedian@eecs.ukans.eduFall 2007
EECS810: Software Engineering (University of Kansas, Fall 2007)Organization of the Tutorial Introduction to Formal Methods (10 Minutes) Introduction to Z with Case Studies (3 Hours) Formal Methods/Z Resources (10 Minutes) Discussion (10 Minutes)Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 1
EECS810: Software Engineering (University of Kansas, Fall 2007)Quality Software Software– an executable program– the structure of program components– functionality of an application program– the look and feel of an interface– the program and all associated documents needed tooperate and maintain it Software pervades many aspects of our lives Absolutely essential to improve the software qualityCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 2
EECS810: Software Engineering (University of Kansas, Fall 2007)What is Quality? A key issue in the field of information technology Multi-dimensional concept with different levels ofabstraction Popular views:– subjective, ambiguous, unclear meaning– luxury, class, taste– difficult to define and measure Professional view– quantifiable– manageable– improveableCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 3
EECS810: Software Engineering (University of Kansas, Fall 2007)Quality: A Definition Crosby (1979):“Conformance to requirements”Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 4
EECS810: Software Engineering (University of Kansas, Fall 2007)Conformance to Requirements: Implications During the production process, measurements arecontinually taken to determine conformance to the thoserequirements: measurement model project tracking and oversight Managerial aspects validation criteria quality assurance system plans, commitment to improvement The use of process models is encouragedCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 5
EECS810: Software Engineering (University of Kansas, Fall 2007)Conformance to Requirements: Implications (continued) Requirements must be clearly stated such that they cannotbe misunderstood: complete unambiguous verifiableTechnical aspects precise concise consistentThe use of formal methods is encouragedCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 6
EECS810: Software Engineering (University of Kansas, Fall 2007)Formal MethodsDefinitions A notation with a well defined syntax and semantics used tounambiguously specify the requirements of a software system. A formal method is expected to support the proof of correctnessof the final implementation of the software with respect to itsspecification. The formal methods notation is used for formal specification of asoftware system:– As a process: translation of a non-mathematical descriptioninto a formal language– As a product: concise description of the properties of a systemin a language with well defined semantics and formaldeduction supportCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 7
EECS810: Software Engineering (University of Kansas, Fall 2007)Why Formal Methods? To precisely and unambiguously describe the functionalityof a software system at an abstract level that can bereasoned about formally using mathematics (or informallybut rigorously) Precision and unambiguity are essential because for a largeproject many individuals have to agree on the interpretationof the specified functionality in order to produce a correctimplementation.Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 8
EECS810: Software Engineering (University of Kansas, Fall 2007)When to Use Formal MethodsSoftware Development Life Cycle: Requirements analysis Requirements specification– As a process: when the functionality of the software isspecified– As a product: where the expected functionality isrecorded Architectural design Detailed design Implementation TestingCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 9
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 10Requirements Specification as a ght Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Essential Properties of a Specification Document Correctness Completeness Unambiguous (one interpretation) Precision (unnecessary detail suppressed) Verifiable and traceable Independent from design Consistent (no conflicting features) Concise (lack of noise, irrelevant features) AnnotatedCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 11
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 12Essential Properties of a Specification Document (continued)For detailed explanations see [Davis 1993, Chapter 3]Formal methods can assist in achieving most of the essentialproperties; more specifically: Unambiguity Verifiability Consistency Conciseness and Preciseness Annotation (especially true in case of Z notation)Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Claimed Benefits, Drawbacks of Formal Methods Benefits:1. Unambiguous descriptions, i.e., there is one uniqueinterpretation of a model given in a formal notation2. Analyzable products i.e., properties such ascompleteness and consistency can be checked by(automated) mechanisms Drawbacks:1. Mathematical skills, enthusiasm are required2. The development and verification process is costly andeffort-intensive3. Complexity may explode with the dimension of theproblem and can become unmanageableCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 13
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 14Misconceptions about Formal MethodsFormal methods are for program verification only While formal methods can be applied during various stagesof software development, their highest impact would beduring the early stages, i.e., modeling and specificationstages Program verification can be considered a secondary concernCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Misconceptions about Formal Methods (continued)Formal methods are too mathematical Based on mathematics, but the mathematics of formalmethods is not very difficult. Most formal methods arebased on the set theory and predicate logic Symbols can be learned through practice and training Not necessarily more complicated than implementationlanguagesCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 15
EECS810: Software Engineering (University of Kansas, Fall 2007)Misconceptions about Formal Methods (continued)An example in ZLibSystemmembers : P Personshelved : P Bookchecked : Book 7 Personshelved dom checked ran checked members mem : Person #(checked {mem}) MaxLoanCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 16
EECS810: Software Engineering (University of Kansas, Fall 2007)Misconceptions about Formal Methods (continued)Examples in C Production code: [Salus 1994]if (rp - p flag & SSWAP) {rp - p flag & SSWAP;aretu (u.u ssav)} A C declaration: [Kernighan & Ritchie, 1988, p.122]int (*(*X[3])())[5]; Copying string t to s: [Kernighan & Ritchie, 1988, p.105]while (*s *t );Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 17
EECS810: Software Engineering (University of Kansas, Fall 2007)Misconceptions about Formal Methods (continued)Inapplicable to Real Projects A. Hall, Seven Myths of Formal Methods, IEEE Software,September 1990, pp. 11–19. J. Bowen and H. Hinchey (editors), Applications of FormalMethods, Prentice-Hall International, 1995.– Nuclear facility– Instrumentation systems (Z)– Voting system (VDM)– IBM’s CICS (Z, B)– Railroad tracking, training, signaling system, (VDM)– Aerospace monitoring system (Z)Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 18
EECS810: Software Engineering (University of Kansas, Fall 2007)Misconceptions about Formal Methods (continued)– Secure operating system (Larch)– AT&T telephone switching system (Z) Of course more work is needed:– H. Saiedian, et al, An Invitation to Formal Methods, IEEEComputer, April 1996.– H. Saiedian (Guest Editor), Journal of Systems andSoftware, Special Issue on Formal Methods TechnologyTransfer, March 1998.Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 19
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 20Need for Measurements for Formal Methods A large number of formal methods have been proposed A formal method notation comes with some common adviseon how to be used; syntax and semantics are given but littleindication is given on how to use it effectively A given FM is unlikely to be equally effective for all domains Required components of formal methods1. formal syntax and semantics2. conceptual model3. uniform notation of an interface4. sufficient expressive power to express relevant features5. hints and suggestion for refinement, implementation in asystematic wayCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 21Philosophical View of Formal MethodsThe following is from John Rushby’s Talk at LFMW97: In engineering, mathematical models of systems are built sothat the properties of those systems can be predictedthrough the power of calculation.The power of mechanized calculation makes theconstruction of complex or optimized physical systemspossible. Formal methods apply the same ideas to the construction ofthe complex logical design of computer systems:– Build a formal mathematical model of some aspect of asystem– Calculate whether or not the system possess certaindesired propertiesCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 22Need for Measurements for Formal Methods (continued) Only qualitative and anecdotal evidence is available aboutthe benefits and drawbacks For sound and objective cost analysis, a thorough study isneeded to assess the degree to which the benefits anddrawbacks are real Such a study or evidence will greatly help wider introductionof formal methods into industrial practice Currently the choice of one method over another is mostly amatter of personal taste not grounded on any objectiveevidence A strong need for an objective assessment of strength,weakness, application domain, and limitation of variousformal methods to allow meaningful comparison andselectionCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 23Formal Methods Light: An alternative Do not promote full formalization; in most cases a less thancompletely formal approach is more helpful, convincing Integrate with existing, not necessarily formal models andapproachesA formal method should contribute to and benefit from anexisting tool or notationCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Model-Based Formal Methods NotationsModel-based notations Support the development of an abstract model of thesoftware product Support the behavioral description of the abstract model Examples: Z, Object-Z, VDM, LarchCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 24
EECS810: Software Engineering (University of Kansas, Fall 2007)Specification Language Z Jean-Raymond Abrial, late 1970s/early 1980s Under continuing development at the ProgrammingResearch Group, Oxford University A state-based modeling/specification language Set theory, predicate logic Functional specification of sequential systems Object-oriented variations Most popular formal methods notationCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 25
EECS810: Software Engineering (University of Kansas, Fall 2007)Z Schemas The building-block for structuring specifications Graphical notationSchemaNameSignaturePredicates An alternative linear notationSchemaName b [Signature Predicates]Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 26
EECS810: Software Engineering (University of Kansas, Fall 2007)Z Schemas (continued) Signature introduces variables and assigns them settheoretic types — similar to declarations in modernprogramming languages Predicates include expressions that relate the elements ofsignature:– Viewed in terms of invariants, pre- and post-conditions– ANDed by default; order is irrelevantCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 27
EECS810: Software Engineering (University of Kansas, Fall 2007)Identifiers in Z Identifiers may be composed of upper and lower caseletters, digits, and the underscore character; must beginwith a letter Identifiers may have suffixes:– ?means an input variable– !means an output variable–′means a new value (i.e., the after-operation value) Schema identifiers may have prefixes:– – Ξmeans the state has changed (described later)means no change in the state (described later)Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 28
EECS810: Software Engineering (University of Kansas, Fall 2007)An Example of a Z SchemaReservepassengers, passengers ′ : P PERSONp? : PERSON#passengers CAPACITYp? 6 passengerspassengers ′ passengers {p?}#passengers ′ CAPACITYAlternative notation:Reserve b [p? : PERSON ; . p? 6 passengers .]Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 29
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 30Notable Advantages of Z Procedural Abstraction: Schemas only describe what is to bedone; issues relating to “how” are ignored Representational Abstraction: Schemas use high-levelmathematical structures like arbitrary sets, functions, .,without worrying about how these are to be implemented Allow annotation. informal descriptions .S······. complement formal definitions .Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 31Schema CalculusA collection of notational conventions used to manipulateschemas and combine them into composite structures. Provides a framework to develop and present schemas in anincremental fashion, i.e., schemas can be constructed fromexisting schemas.– Analogous to “modular” program development.– Specifications become more manageable. Achieved primarily by means of “Schema Inclusion” and“Schema Linking” and and Ξ conventions.Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Schema Inclusion Suppose we have the following two schemas:schemaAp, q : ZschemaBr, s : Np qr s We can form a new schema by including two existing ones:schemaABschemaAschemaB If “expanded,” SchemaAB will include:schemaABp, q : Z; r , s : Np q r sCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 32
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 33Schema Linking It is possible to use propositional connectives (e.g., , , , ) and existing schemas to construct a new one. We can construct schemaBA as follows:schemaBA b schemaA schemaB If “expanded,” schemaBA will include:schemaBAp, q : Zr, s : Np q r sCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007) and Ξ ConventionsOperations and changes in the state data:State BeforeOperationState AfterCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 34
EECS810: Software Engineering (University of Kansas, Fall 2007) and Ξ Conventions (continued)Thus, to define an operation we must have:OperationStateDataStateData ′Predicates describing StateDataPredicates describing StateData ′Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 35
EECS810: Software Engineering (University of Kansas, Fall 2007) and Ξ Conventions (continued)Consider operation Reserve again:Reservepassengers, passengers ′ : P PERSONp? : PERSON#passengers CAPACITYp? 6 passengerspassengers ′ passengers {p?}#passengers ′ CAPACITYCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 36
EECS810: Software Engineering (University of Kansas, Fall 2007) and Ξ Conventions (continued)Slide 37 Conventionally, two schemas are given to define the state ofdata, one describing state before an operation, and one fordescribing state after the operation. For a simple reservation system we may have:ResSystpassengers : P PERSONResSyst ′passengers ′ : P PERSON#passengers CAPACITY#passengers ′ CAPACITYCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007) and Ξ Conventions (continued) Reserve operation can now be specified as:ReserveResSystResSyst ′p? : PERSON#passengers CAPACITYp? 6 passengerspassengers ′ passengers {p?}Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 38
EECS810: Software Engineering (University of Kansas, Fall 2007) and Ξ Conventions (continued) While most operations bring about changes in the statedata, some do not:PassengerCountResSystResSyst ′count ! : Ncount ! #passengersCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)Slide 39
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 40 and Ξ Conventions (continued) convention is commonly used to represent change ofstate; it combines the definitions of two schemas, onedescribing the state before an operation and one describingthe state after the operation: ResSystResSystResSyst ′ Ξ convention is commonly used to represent no change ofstate; it can be defined in terms of :ΞResSyst ResSystpassengers passengers ′Copyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007) and Ξ Conventions (continued)Slide 41 Operation Reserve can now be specified using convention:Reserve ResSystp? : PERSON#passengers CAPACITYp? 6 passengerspassengers ′ passengers {p?} Similarly, operation PassengerCount can now be specifiedusing Ξ convention:PassengerCountΞResSystcount ! : Ncount ! #passengersCopyright Saiedian 2007 (For exclusive use of EECS Software Engineering Students)
EECS810: Software Engineering (University of Kansas, Fall 2007)Slide 42 and Ξ Conventions (Summary) The prefix denotes a new schema built by combining thebefore and after specification of a state
A formal method is expected to support the proof of correctness of the final implementation of the software with respect to its specification. The formal methods notation is used for formal specification of a software system: – As a process: translation of a non-mathematical description into a formal language
Reasoning about Metamodeling with Formal Speci cations and Automatic Proofs Ethan K. Jackson1, Tihamer Levendovszky 2, and Daniel Balasubramanian 1Microsoft Research, Redmond, WA and 2Vanderbilt University, Nashville, TN ejackson@microsoft.com
Packaging Speci cations Code Part No. Code Tolerance Packaging Speci cations Reel Basic Ordering Unit (pcs) Remarks J( 5 %) F( 1) MCR01S MQP Paper tape (2mm Pitch) 180mm (7inch) 10,000 — MCR03S EQP Paper tape (4mm Pitch) 180mm (7inch) 5,000 — MCR10S EQP Paper tape (4mm Pitch) 180mm (7inch) 5,000 —
Prices Effective January 1, 2020 Machine Prices and Speci cations Prices Effective January 1, 2020 ZERO TURN-4 SERIES REVISED MAY 18, 2020. Machine Prices and Secications Prices Eectie anuar , 2 ZT1. Prices F.O.B. Selma, Alabama and Subject to Change Without Notice. ESTATE SERIES
Identify commonly used listed and labeled equipment (UL or CSA) Blueprints, Speci cations, and Estimations Identify and interpret electrical symbols and speci cations in blueprints and plan symbols Identify and interpret wiring and schematic diagrams Demonstrate planning and layout of a circuit AC/DC Theory
M7V Series Variable Displacement Type Axial Piston Motors Speci cations and Features 8 1. Ordering Code 9 2. Technical Information 2-1. Speci cations 12 2-2. Precautions for System Design 13 2-3. Speed Sensor 14 2-4. Accessory 15 3. Regulators 3-1. Two Position Displacement Control 17 3-2. Proportional Displacement Control 21 3-3.
CRYSTALS-Kyber Algorithm Speci cations And Supporting Documentation (version 2.0) Roberto anzi,vA Joppe Bos, Léo Ducas, Eike Kiltz, ancrèdeT Lepoint, adimV Lyubashevsky, John M. Schanck, Peter Schwabe, Gregor Seiler, Damien Stehlé April 1, 2019 1
Doleisch, Gasser, Hauser / Interactive Feature Speci cation for F C Visualization of Complex Simulation Data Figure 1: Flexible Feature Speci cation: simulation data of a catalytic converter is shown, two features have been speci ed based on our feature de nition language, using the different views for interaction and visualization.
2. Lubin-Tate spaces 45 2.1. The height of a formal A-module 46 2.2. Lubin-Tate spaces via formal group laws 49 2.3. Lazard's theorem for formal A-modules 52 2.4. Proof of the lemma of Lazard and Drinfeld 60 2.5. Consequences for formal A-modules 66 2.6. Proof of representability of Lubin-Tate spaces 76 3. Formal schemes 82 3.1. Formal .
