Book Chapters by Ian Hayes

[1] Eban Escott, Paul Strooper, Paul King, and Ian Hayes. Model-driven web form validation with UML and OCL. In Andreas Harth and Nora Koch, editors, Current Trends in Web Engineering, volume 7059 of Lecture Notes in Computer Science, pages 223--235. Springer Berlin / Heidelberg, 2012. [bib| http]
Form validation is an integral part of a web application. Web developers must ensure that data input by the user is validated for correctness. Given the importance of form validation it must be considered as part of a model-driven solution to web development. Existing model-driven approaches typically have not addressed form validation as part of the model. In this paper, we present an approach that allows validation constraints to be captured within a model using UML and OCL. Our approach covers three common types of validation: single element, multiple element, and entity association. We provide an example to illustrate an architecture-centric approach.
[2] IanJ. Hayes. Dynamically detecting faults via integrity constraints. In Michael Butler, Cliff Jones, Alexander Romanovsky, and Elena Troubitsyna, editors, Methods, Models, and Tools for Fault Tolerance, volume 5454 of Lecture Notes in Computer Science, pages 85--103. Springer Verlag, 2009. [bib]
Control programs for safety-critical systems are required to tolerate faults in the devices they control. In this paper we examine a systematic approach to devising code to detect faulty devices at runtime. The approach is centred around the use of integrity constraints, which are invariants on the state of a system's variables, including its inputs and outputs. Under normal operation integrity constraints should always hold, but they are designed to fail to hold if there is a fault. By adding variables to capture the previous state of variables or the time of significant events, additional integrity constraints can be devised to check for faults in state transitions or faults with the rate of progress of the system. We discuss techniques for devising integrity constraints as well as efficiently evaluating the constraints. When an error is detected via the failure of an integrity constraint, the integrity constraint(s) that failed can help diagnose the likely fault. We illustrate the approach using controller software written in the action system style, but it is equally applicable to other state machine approaches such as Event-B and TLA.
[3] R.Colvin, L.Groves, I.J. Hayes, D.Hemer, R.Nickson, and P.A. Strooper. Developing logic programs from specifications using stepwise refinement. In Maurice Bruynooghe and Kung-Kiu Lau, editors, Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, volume 3049 of Lecture Notes in Computer Science, pages 66--89. Springer Verlag, 2004. [bib]
In this paper we demonstrate a refinement calculus for logic programs, which is a framework for developing logic programs from specifications. The paper is written in a tutorial-style, using a running example to illustrate how the refinement calculus is used to develop logic programs. The paper also presents an overview of some of the advanced features of the calculus, including the introduction of higher-order procedures and the refinement of abstract data types.
[4] I.J. Hayes. A predicative semantics for real-time refinement. In A.McIver and C.C. Morgan, editors, Programming Methodology, pages 109--133. Springer, 2003. [bib]
Real-time systems play an important role in many safety-critical systems. Hence it is essential to have a formal basis for the development of real-time software. In this chapter we present a predicative semantics for a real-time language. The semantics includes a special variable representing the current time, and uses timed traces to present the values of external input and outputs over time so that reactive control systems can be handled. Because a real-time control system may be a nonterminating process, we allow the specification of nonterminating programs and the development of nonterminating repetitions.
[5] I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. In J.P. Bowen and M.G. Hinchey, editors, High-Integrity System Specification and Design, pages 563--581. Springer, 1999. (Previously published in IEE/BCS Software Engineering Journal, Vol. 4, No. 6, 330--338, November, 1989). [bib]
[6] I.J. Hayes. CICS message system. In I.J. Hayes, editor, Specification Case Studies, pages 238--243. Prentice Hall International, second edition, 1993. [bib]
[7] I.J. Hayes. CICS temporary storage. In I.J. Hayes, editor, Specification Case Studies, pages 226--237. Prentice Hall International, second edition, 1993. [bib]
[8] I.J. Hayes. Applying formal specification to software development in industry. In I.J. Hayes, editor, Specification Case Studies, pages 181--201. Prentice Hall International, second edition, 1993. (Previously published in IEEE Transactions on Software Engineering [?]). [bib]
[9] I.J. Hayes. Flexitime specification. In I.J. Hayes, editor, Specification Case Studies, pages 134--138. Prentice Hall International, second edition, 1993. [bib]
[10] I.J. Hayes. Block-structured symbol table. In I.J. Hayes, editor, Specification Case Studies, pages 14--30. Prentice Hall International, second edition, 1993. [bib]
[11] I.J. Hayes. Examples of specification using mathematics. In I.J. Hayes, editor, Specification Case Studies, pages 2--13. Prentice Hall International, second edition, 1993. [bib]
[12] I.J. Hayes. Applying formal specification to software development in industry. In RichardH. Thayer and Merlin Dorfman, editors, System and Software Requirements Engineering, pages 594--603. IEEE Computer Society Press Tutorial, 1990. (Previously published in IEEE Transactions on Software Engineering [?]). [bib]

This file was generated by bibtex2html 1.99.

Last updated: Wed 3 Jan 2024 17:12:52 AEDT