CSC3332 : Abstract Models of Systems and Languages (Inactive)
- Inactive for Year: 2023/24
- 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.
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 Study | Assessment preparation and completion | 40 | 1:00 | 40:00 | Lecture follow-up |
| Scheduled Learning And Teaching Activities | Lecture | 12 | 2:00 | 24:00 | Traditional lectures PIP |
| Guided Independent Study | Assessment preparation and completion | 1 | 25:00 | 25:00 | Revision to end of semester exam and exam duration |
| Scheduled Learning And Teaching Activities | Practical | 12 | 2:00 | 24:00 | Computer classroom PIP |
| Guided Independent Study | Project work | 1 | 25:00 | 25:00 | Coursework |
| Guided Independent Study | Independent study | 62 | 1:00 | 62:00 | Background reading |
| Total | 200: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 Examination | 120 | 1 | A | 50 | N/A |
Other Assessment
| Description | Semester | When Set | Percentage | Comment |
|---|---|---|---|---|
| Practical/lab report | 1 | M | 50 | Models and programs. |
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
- Timetable Website: www.ncl.ac.uk/timetable/
- CSC3332's Timetable