module specification

The module introduces a model based approach to the construction 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.

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

Logic and Mathematical Techniques or Logic and Problem Solving or Mathematical Proofs

• 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.Software Implementation
• Non-deterministic finite automata. Algorithm for converting NFAs to DFAs. Software Implementation
• 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.Using regular expressions in programming
• Context free grammars. Introduction and notation. Derivations and syntax trees. Ambiguity in CFGs. Expressive power of FAs and CFGs. PDA implementation.
• 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, HCL 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.Integration of semantic repositories.
• Ontological Engineering. Semantic technologies, software architectures and development tools for construction of semantically enabled systems.

Learning Outcomes LO1 - LO6

The module will be taught by a series of lectures, supervised laboratory, self-study and in class practical exercises. The lectures will be used to formally introduce the concepts and principles. The supervised practical sessions and/or seminars will provide opportunities 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 pieces of coursework and two class tests.

Coursework 1 and 2 are based on two case studies where the requirements are provided through an informal description.  Both pieces of coursework will have a group work 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 pieces of coursework 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

• Coursework 1 consists of producing a formal specification from the case study requirements and its implementation
• Coursework 2 consists of formal specification and its implementation

The two class tests assess the students’ knowledge, understanding and use of formal specification, modelling and software implementation at the end of each semester.

Online Reading List:

https://londonmet.rl.talis.com/lists/C808AD20-06FA-9C9B-4859-22A3D47E78E1.html

Textbooks:

Core Text:
• Adam Brooks Webber. Formal Language: A Practical Introduction. Franklin, Beedle & Associates, Inc. (2011); ISBN: 9781590281970.
• Michael Huth, Mark Ryan. Logic in Computer Science: Modeling and Reasoning about Systems. Cambridge University Press, 2nd edition (2004); ISBN: 052154310X.
• Grigoris Antoniou, Paul Groth, Frank Van Harmelen, Rinke Hoekstra. A Semantic Web Primer. MIT Press, 3rd edition (2012); ISBN: 0262018284.

Other Texts:
• Franz Baader, Ian Horrocks, Carsten Lutz, Uli Sattler. An Introduction to Description Logic, Cambridge University Press (2017); ISBN: 9780521695428
• Elaine A. Rich. Automata, Computability and Complexity: Theory and Applications. Prentice Hall, 1st edition (2007);  ISBN: 0132288060.
• Dean Allemang, Jim Hendler. Semantic Web for the Working Ontologist, 2nd ed. Morgan Kaufmann (2011); ISBN: 9780123859655.
Journals:
• ACM Transactions on Software Engineering and Methodology (TOSEM), Publisher: Association for Computing Machinery (ACM), ISSN: 1049331X
https://tosem.acm.org/
Websites:
• Safari Books Online
Electronic Databases (available from the University Library)
• ACM Digital Library
• IEEE Xplore/IET Digital Library
Other
• Lynda.com