module specification

The module introduces a model based approach to the constraction of software systems using formal specification languages as a basis for the software development. It will provide students with the knowledge and skills to produce formal specifications from informal descriptions and to implement them using appropriate programming techniques.

• MA4001 Logic and Problem Solving OR MA4005 Logic and Mathematical Techniques or equivalent
• CS5003 Data Structures and Specialist Programming
 

The module aims are to:

• Introduce model based formal specification languages
• Provide students with the knowledge and skills to construct formal specifications from informal descriptions
• Provide understanding of techniques used in the design and implementation of software systems and relating the principles to real world and practical examples
• Refine formal specifications for implementation and implement them

• Words, alphabets and languages. Operations on words and languages. Closure of languages.
• Deterministic finite automata. DFAs as language recognisers. Equivalent DFAs. Completion of DFAs. The DFA Pumping Lemma. Simplification and minimisation of DFAs.
• Non-deterministic finite automata. Algorithm for converting NFAs to DFAs.
• Distinguishable and indistinguishable states. Union, catenation and closure of finite automata. Intersection of two FAs.
• Introduction to regular expressions. Examples and notation. Converting FA to regular expressions and vice versa. Expressive power and equivalence of regular expressions and FAs.
• Context free grammars. Introduction and notation. Derivations and syntax trees. Ambiguity in CFGs. Expressive power of FAs and CFGs.
• Simplification of CFGs. Binary Form, Chomsky Normal Form.
• Universal computational machines. Turing machines and the Halting Problem.
• Syntax and semantics of logical languages – Propositional Logic, Predicate Logic, Description Logic.
• Semantic models and validation of logical theories. Satisfiability, truth and completeness. Logical verification.
• Inference rules and logical reasoning in logical theories. Entailment, contradiction and consistency. Logical proof and refutation.
• Using symbolic logics for formal specification. FOL and DL as specification languages. Vocabulary of terms, facts, constraints and heuristics.
• Automated reasoning. Clausal form and skolemization. Unification, Resolution and Subsumption.
• Semantic Web. RDF, OWL and SWRL and serialization of logical languages in XML.
• Querying semantic repositories. SPARQL.
• Ontological Engineering. Semantic technologies, software architectures and development tools for construction of semantically enabled systems.

The module will be taught by a series of lectures, supervised laboratory, self-study and inclass practical exercises. The lectures will be used to formally introduce the concepts and principles. The supervised practical sessions and/or seminars will provide oppertunities to apply and experiment with the ideas introduced. The students will also be required to undertake independent study, for example individual and group case studies, some of which will be part of the assessment for the module.

On completing the module the student should be able:

LO1 Demonstrate understanding of the advantages of using formal specification
LO2 Develop formal specifications from informal problem statements
LO3 Demonstrate understanding of specifications written by others
LO4 Describe and recognise  the characteristics of major established architecture styles
LO5 Design and construct software that satisfies a formal or informal specification
LO6 Evaluate the quality of their specification and implementation
LO7 Evaluate their experiences of group work, the processes of producing their coursework and the product produced

This module is assessed through two courseworks and two class tests.

Courseworks 1 and 2 are based on two case studies where the requirements are provided through an informal description.  Both courseworks will have a groupwork part to encourage communication, critical analysis and creative thinking, and an individual work part to assess the practical skills in developing software after formal specification. Both courseworks are assessed by report, product and viva. The report will include a reflective element by each student on the operation of the group, their work within the group, the quality of the product and what they learnt and discovered [LO7].
Coursework 1 consists of producing a formal specification from the case study requirements and its implementation [LO1, LO2, LO3, LO5, LO6, LO7].
Coursework 2 consists of formal specification and its implementation [LO1, LO2, LO3, LO5, LO6, LO7]
The two class tests assess the students’ knowledge, understanding and use of formal specification, modeling and software implementation at the end of each semester. [LO1 to 6].

Core Textbooks

[1] Adam Brooks Webber. Formal Language: A Practical Introduction. Franklin, Beedle & Associates, Inc. (2008); ISBN: 9781590281970 CORE
[2] Michael Huth, Mark Ryan. Logic in Computer Science: Modeling and Reasoning about Systems. Cambridge University Press, 2nd edition (2004);  ISBN: 052154310X CORE
[3] Franz Baader, Ian Horrocks, Carsten Lutz, Uli Sattler. An Introduction to Description Logic, Cambridge University Press (2017); ISBN: 9780521695428 CORE
[4]  Grigoris Antoniou, Paul Groth, Frank Van Harmelen, Rinke Hoekstra. A Semantic Web Primer. MIT Press, 3rd edition (2012); ISBN: 0262018284 CORE

Further reading:
[1] Elaine A. Rich. Automata, Computability and Complexity: Theory and Applications. Prentice Hall, 1st  edition (2007);  ISBN: 0132288060
[2] Péter Szeredi, Gergely Lukácsy, Tamás Benkö. The Semantic Web Explained: The Technology and Mathematics behind Web 3.0. Cambridge University Press (2014); ISBN: 0521700361
[3] Dean Allemang, Jim Hendler. Semantic Web for the Working Ontologist, 2nd ed. Morgan Kaufmann (2011); ISBN: 9780123859655