Skip to main content

Module

CSC3332 : Abstract models of systems & Languages

  • Offered for Year: 2022/23
  • Module Leader(s): Dr Leo Freitas
  • Owning School: Computing
  • Teaching Location: Newcastle City Campus
Semesters
Semester 1 Credit Value: 20
ECTS Credits: 10.0

Aims

Using models to understand complicated systems is a standard process in engineering. The key skill is abstraction (leaving out details to focus on key properties). The principal aim of this module is to communicate this skill.

In order to record models, it is necessary to use some notation. There are several notations, and they tend to have areas of application. If the notation is well thought out, it makes it possible to reason about properties of the described system; If there is mechanical support, one can both exercise the model and draw verified conclusions.

The range of applications of interest range from simple components to aircraft collision avoidance.

A particular focus will be on recording the meaning (semantics) of programming languages.
Programming languages come and go - if you make a career in computing, there is no doubt that you will have to learn languages which do not even exist today. In addition to literally thousands of existing general purpose languages, there are languages tailored for specific applications, such as gaming, virtual reality, text layout, robotics. Sadly, many languages embody one new idea (e.g. objects, concurrency, remote execution), but are significantly *worse* than their predecessors in other respects.

A key aim of this module is to communicate ways of understanding and documenting the main ideas in a language. The material should equip you to make sense of the many languages you will meet in your career. If you design new languages, they will benefit from you being able to manipulate the key concepts.

Furthermore, to make sure the complexities (and scale) of language design are addressed, you will also be trained in practical aspects of formal modelling and verification. For this we will use a well- founded approach following a set of mature formal tools and techniques within software engineering

Outline Of Syllabus

Modelling and Specification
-       Key notion of abstraction: pre/post conditions and data abstraction
-       Reasoning about a model
-       Checking that an implementation corresponds to a model
-       Notions of functional programming: induction, recursion, datatypes, etc.
-       Animating versus reasoning about a model
-       Basics notions of verification tools: Isabelle 101, tooling for language design.
-       Elicitation and basic proof of simple properties of interest
-       Code-contracts and programming correctness-reasoning

Programming languages
-       - syntax versus semantics
-       - concrete versus abstract syntax;
-       - context conditions
- Semantics (meaning) focus on the "Structural Operational Semantics"
-       Improved language-design decisions: type system extensions (e.g. security-types, etc.), feature extension (e.g. OO + concurrency), etc.

-       General
-       nature of software verification principles (correctness, abstraction, refinement, design decisions, documented assumptions, model-based testing, etc.)
-       understanding the expertise required and costs involved, identifying the right technique to the task at hand.

Teaching Methods

Teaching Activities
Category Activity Number Length Student Hours Comment
Guided Independent StudyAssessment preparation and completion125:0025:00Revision to end of semester exam and exam duration
Scheduled Learning And Teaching ActivitiesLecture122:0024:00Traditional lectures PIP
Guided Independent StudyAssessment preparation and completion401:0040:00Lecture follow-up
Scheduled Learning And Teaching ActivitiesPractical122:0024:00Computer classroom PIP
Guided Independent StudyProject work125:0025:00Coursework
Guided Independent StudyIndependent study621:0062:00Background reading
Total200:00
Teaching Rationale And Relationship

Lectures are used to impart knowledge and practicals are used to provide experience of the solution of problems and understanding of decisions in practice.

Assessment Methods

The format of resits will be determined by the Board of Examiners

Exams
Description Length Semester When Set Percentage Comment
Written Examination901A50N/A
Other Assessment
Description Semester When Set Percentage Comment
Practical/lab report1M50Models, programs and proofs.
Assessment Rationale And Relationship

The unseen examination will allow assessment of acquired knowledge using short bookwork questions, the ability to apply that knowledge using application questions, & time-constrained assessment of subject-specific skills using application questions.

The coursework will allow in-depth assessment of cognitive and subject-specific programming skills.

There is one system design and analysis assignment assessing the understanding of basic concepts of the modelling and analysis of concurrent systems through a simple case study using the Workcraft toolkit developed at Newcastle. The coursework will involve design of a model, its implementation as a Petri net, formulation of analytical requirements, and automatic checking of these requirements.

The examination is based around theoretical issues involved in a problem solving task. It is an "open book" examination paper: nothing needs to be memorised to pass.

The purpose of the problem solving exercises is to familiarise the students with the software for modelling and verification of complex systems, and to practice the modelling techniques learnt at the lectures.

N.B. This module has both “Exam Assessment” and “Other Assessment” (e.g. coursework). If the total mark for either assessment falls below 35%, the maximum mark returned for the module will normally be 35%.

Reading Lists

Timetable