Jon Nicholson. Phd. FHEA. CTO. Educator. Coder.

Experience

Industry

As Chief Technology Officer at ZiNET Data Solutions Limited I lead a team developing new products in the data and education sectors such as dataexchange.education, which enables schools, local authorities, multi academy trusts and application vendors to use data securely and effectively by integrating multiple systems. Attribute level permissions and digitally signed data sharing agreements means institutions are in full control of the data they share. DataExchange is built with SIF Open Standards at its core. I have also been working on opendata.education, which consolidates and simplifies access to open data in the education sector of the UK. Information from open sources such as Edubase and data.gov.uk are processed and shared using an open, publicly accessible, API. OpenData is built with SIF Open Standards at its core, is a 5-star linked data resource, and has Gold-level Open Data Institute certification.

I sit on the Global Infrastructure Group, working to improve the SIF infrastructure definition, and the Open Source Developers Network, working to facilitate and support open source projects using SIF, within A4L (Access 4 Learning) Community.

Previous roles include Senior Lecturer at the University of Brighton, and Consultant Developer for SchoolsICT.

Research

My PhD (University of Essex, 2011) was on the formal specification and verification of object-oriented design statements. I studied under Professor Raymond Turner and Dr Amnon H. Eden and was funded by an EPSRC Doctoral Training Award.

In September 2014 I applied for my EPSRC First Grant as Principal Investigator on proposal entitled “Querying Ontologies with Diagrams” (£125k). The project was partnered with Nokia and would have looked how Concept Diagrams could be used to define and visualize the results of SPARQL (semantic web) queries. The proposal was well received by reviewers, but ultimately did not secure funding. I was also included as an early career researcher in the University of Brighton's Research Excellence Framework (REF) 2014 submission to Computer Science and Informatics.

Between 2015 and 2017 I was involved in a Knowledge Transfer Partnership with a company called Colony101 developing novel visual approaches to the management of marketing life cycles resulting in a new product called Cyclr.

Teaching

I began teaching in 2006 as graduate teaching assistant, and became a lecturer in 2011 at the University of Brighton. In 2013 I received a postgraduate certificate in Teaching and Learning in Higher Education from the University of Brighton, through which I became a Fellow of the Higher Education Academy later that year.

From January 2016 until leaving the University of Brighton I was the Computing Strand Leader for the Joint Honours courses at the Hastings campus, and was Course Leader for BSc (hons) Digital Games Production for the 2013-2014 academic year. I have taught a variety of code and design based subjects, mainly focussed around web and mobile technologies.

Qualifications

PGCert Learning and teaching in higher education, Pass with Merit, University of Brighton, UK, 2013.
PhD, Computer Science, University of Essex, Colchester, UK, 2011.
MSc Computer Science (Distributed Information Management Systems), Pass with Distinction, University of Essex, UK, 2006.
BSc (Hons) Computer Science, First Class, University of Essex, UK, 2005.

Publications

Below is a complete list of my publications, which you can download in BibTeX format.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author’s copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Journals

2017

A. H. Eden, E. Gasparis, J. Nicholson, and R. Kazman, Round-trip engineering with the two-tier programming toolkit. Software quality journal, :1-23, 2017.

[Abstract] [BibTex] [Link]

Abstract

A major impediment to the long-term quality of large and complex programs is inconsistency between design and implementation. Conflicts between intent and execution are common because detecting them is laborious, error-prone, and poorly supported, and because the costs of continuously maintaining design documents outweigh immediate gains. A growing inconsistency between design and implementation results in software that is unpredictable and poorly understood. Round-trip engineering tools support an iterative process of detecting conflicts and resolving them by changing either the design or the implementation. We describe a Toolkit which supports a round-trip engineering of native Java programs without interfering with any existing practices, tools, or development environments, thereby posing a minimal barrier on adoption. The Toolkit includes a user-guided software visualization and design recovery tool, which generates Codecharts from source code. A ``round-trip'' process is possible because Codecharts visualizing source code can be edited to reflect the intended design, and the Verifier can detect conflicts between the intended and as-implemented design. We demonstrate each stage in this process, showing how the Toolkit effectively helps to close the gap between design and implementation, recreate design documentation, and maintaining consistency between intent and execution.

BibTex

@article{eden_rtwttpt,
author = "Amnon H. Eden and Epameinondas Gasparis and Jon Nicholson and Rick Kazman",
title = "Round-trip engineering with the Two-Tier Programming Toolkit",
journal = "Software Quality Journal",
issn = "1573-1367",
month = "may",
year = "2017",
pages = "1--23",
doi = "10.1007/s11219-017-9363-9",
url = "https://doi.org/10.1007/s11219-017-9363-9",
abstract = "A major impediment to the long-term quality of large and complex programs is inconsistency between design and implementation. Conflicts between intent and execution are common because detecting them is laborious, error-prone, and poorly supported, and because the costs of continuously maintaining design documents outweigh immediate gains. A growing inconsistency between design and implementation results in software that is unpredictable and poorly understood. Round-trip engineering tools support an iterative process of detecting conflicts and resolving them by changing either the design or the implementation. We describe a Toolkit which supports a round-trip engineering of native Java programs without interfering with any existing practices, tools, or development environments, thereby posing a minimal barrier on adoption. The Toolkit includes a user-guided software visualization and design recovery tool, which generates Codecharts from source code. A ``round-trip'' process is possible because Codecharts visualizing source code can be edited to reflect the intended design, and the Verifier can detect conflicts between the intended and as-implemented design. We demonstrate each stage in this process, showing how the Toolkit effectively helps to close the gap between design and implementation, recreate design documentation, and maintaining consistency between intent and execution."
}

2014

J. Nicholson, A. H. Eden, R. Kazman, and E. Gasparis, Automated verification of design patterns: a case study. Science of computer programming, 80(Part B):211-222, 2014.

[Notes] [Abstract] [BibTex] [Link]

Abstract

Representing design decisions for complex software systems, tracing them to code, and enforcing them throughout the lifecycle are pressing concerns for software architects and developers. To be of practical use, specification and modeling languages for software design need to combine rigor with abstraction and simplicity, and be supported by automated design verification tools that require minimal human intervention. This paper examines closely the use of the visual language of Codecharts for representing design decisions and demonstrate the process of verifying the conformance of a program to the chart. We explicate the abstract semantics of segments of the Java package java.awt as a finite structure; specify the Composite design pattern as a Codechart and unpack it as a set of formulas; and prove that the structure representing the program satisfies the formulas. We also describe a set of tools for modeling design patterns with Codecharts and for verifying the conformance of native (plain) Java programs to the charts.

BibTex

@article{nicholson_avdpacs,
author = "Jon Nicholson and Amnon H. Eden and Rick Kazman and Epameinondas Gasparis",
title = "Automated verification of design patterns: A case study",
journal = "Science of Computer Programming",
volume = "80",
number = "Part B",
issn = "0167-6423",
month = "feb",
year = "2014",
pages = "211--222",
doi = "10.1016/j.scico.2013.05.007",
url = "http://www.sciencedirect.com/science/article/pii/S0167642313001354",
abstract = "Representing design decisions for complex software systems, tracing them to code, and enforcing them throughout the lifecycle are pressing concerns for software architects and developers. To be of practical use, specification and modeling languages for software design need to combine rigor with abstraction and simplicity, and be supported by automated design verification tools that require minimal human intervention. This paper examines closely the use of the visual language of Codecharts for representing design decisions and demonstrate the process of verifying the conformance of a program to the chart. We explicate the abstract semantics of segments of the Java package java.awt as a finite structure; specify the Composite design pattern as a Codechart and unpack it as a set of formulas; and prove that the structure representing the program satisfies the formulas. We also describe a set of tools for modeling design patterns with Codecharts and for verifying the conformance of native (plain) Java programs to the charts.",
note = "Originally published online (early access) in May 2013."
}

2013

A. H. Eden, E. Gasparis, J. Nicholson, and R. Kazman, Modeling and visualizing object-oriented programs with codecharts. Formal methods in system design, 43(1):1-28, 2013.

[Abstract] [BibTex] [Link]

Abstract

Software design, development and evolution commonly require programmers to model design decisions, visualize implemented programs, and detect conflicts between design and implementation. However, common design notations rarely reconcile theoretical concerns for rigor and minimality with the practical concerns for abstraction, scalability and automated verifiability. The language of Codecharts was designed to overcome these challenges by narrowing its scope to visual specifications that articulate automatically-verifiable statements about the structure and organization of object-oriented programs. The tokens in its visual vocabulary stand for the building-blocks of object-oriented design, such as inheritance class hierarchies, sets of dynamically-bound methods, and their correlations. The formalism was tailored for those pragmatic concerns which arise from modeling class libraries and design patterns, and for visualizing programs of any size at any level of abstraction. We describe design verification, a process of proving or refuting that a Java program (i.e. its native code) conforms to the Codechart specifying it. We also describe a toolkit which supports modeling and visualization with Codecharts, as well as a fully-automated design verification tool. We conclude with empirical results which suggest gains in both speed and accuracy when using Codecharts in software design, development and evolution.

BibTex

@article{eden_mvoopc,
author = "Amnon H. Eden and Epameinondas Gasparis and Jonathan Nicholson and Rick Kazman",
title = "Modeling and visualizing object-oriented programs with Codecharts",
journal = "Formal Methods in System Design",
issn = "0925-9856",
volume = "43",
number = "1",
month = "jan",
year = "2013",
pages = "1--28",
publisher = "Springer",
doi = "10.1007/s10703-012-0181-1",
url = "http://www.eden-study.org/articles/2013/Modeling_and_Visualizing_OO_Programs_with_Codecharts_FMSD.pdf",
abstract = "Software design, development and evolution commonly require programmers to model design decisions, visualize implemented programs, and detect conflicts between design and implementation. However, common design notations rarely reconcile theoretical concerns for rigor and minimality with the practical concerns for abstraction, scalability and automated verifiability. The language of Codecharts was designed to overcome these challenges by narrowing its scope to visual specifications that articulate automatically-verifiable statements about the structure and organization of object-oriented programs. The tokens in its visual vocabulary stand for the building-blocks of object-oriented design, such as inheritance class hierarchies, sets of dynamically-bound methods, and their correlations. The formalism was tailored for those pragmatic concerns which arise from modeling class libraries and design patterns, and for visualizing programs of any size at any level of abstraction. We describe design verification, a process of proving or refuting that a Java program (i.e. its native code) conforms to the Codechart specifying it. We also describe a toolkit which supports modeling and visualization with Codecharts, as well as a fully-automated design verification tool. We conclude with empirical results which suggest gains in both speed and accuracy when using Codecharts in software design, development and evolution."
}

Books and book chapters

2011

A. H. Eden and J. Nicholson, Codecharts: roadmaps and blueprints for object-oriented programs, Wiley-Blackwell, 2011.

[BibTex] [Link]

Conferences and workshops

2017

J. Nicholson and I. Tasker, "(forthcoming) dataexchange: privacy by design for data sharing in education," in 1st international conference on the frontiers and advances in data science, Xi'An, China, 2017.

[BibTex]

2014

A. Delaney, E. Kow, P. Chapman, and J. Nicholson, "Generating and navigating large euler diagrams," in 4th international workshop on euler diagrams, Melbourne, Australia, 2014, pages 23-31.

[Notes] [BibTex]

BibTex

@inproceedings{delaney_gnled,
author = "Aidan Delaney and Eric Kow and Peter Chapman and Jon Nicholson",
title = "Generating and Navigating Large Euler Diagrams",
pages = "23--31",
booktitle = "4th International Workshop on Euler Diagrams",
publisher = "CEUR-WS.org",
series = "CEUR-WS",
volume = "1244",
address = "Melbourne, Australia",
month = "jul",
year = "2014",
note = "Workshop was part of the Diagrams 2014 conference."
}

2012

J. Nicholson, A. Delaney, and G. Stapleton, "Linking codecharts with programs," in Ieee symposium on visual languages and human-centric computing, Innsbruck, Austria, 2012, pages 259-260.

[Abstract] [BibTex]

Abstract

Codecharts are expressively lightweight whilst sufficiently rich to develop insight into program design. This paper contributes an informal description of the semantics of codecharts using the abstract syntax defined in [Nicholson et al., Formalizing the Syntax of Codecharts]. Future work is to further formalize the semantics, define an inference system in which to prove soundness and completeness, and to investigate applications. In particular, we believe that some interesting program metrics, ascertaining program complexity or the level of dependencies and coupling present, can be readily defined and visualized using codecharts. For instance, we can make the area of an ellipse proportional the level of coupling, with relatively large ellipses indicating the need to consider refactoring. Such applications of codecharts could lead to improved software design and understanding.

BibTex

@inproceedings{nicholson_lcwp,
author = "Jon Nicholson and Aidan Delaney and Gem Stapleton",
title = "Linking codecharts with programs",
pages = "259--260",
booktitle = "IEEE Symposium on Visual Languages and Human-Centric Computing",
publisher = "IEEE",
address = "Innsbruck, Austria",
month = "sep",
year = "2012",
doi = "10.1109/VLHCC.2012.6344543",
abstract = "Codecharts are expressively lightweight whilst sufficiently rich to develop insight into program design. This paper contributes an informal description of the semantics of codecharts using the abstract syntax defined in [Nicholson et al., Formalizing the Syntax of Codecharts]. Future work is to further formalize the semantics, define an inference system in which to prove soundness and completeness, and to investigate applications. In particular, we believe that some interesting program metrics, ascertaining program complexity or the level of dependencies and coupling present, can be readily defined and visualized using codecharts. For instance, we can make the area of an ellipse proportional the level of coupling, with relatively large ellipses indicating the need to consider refactoring. Such applications of codecharts could lead to improved software design and understanding."
}

J. Nicholson and A. Delaney, "Formalising simple codecharts," in 7th international conference on the theory and application of diagrams, Canterbury, UK, 2012, pages 346-348.

[Abstract] [BibTex]

BibTex

@inproceedings{nicholson_fsc,
author = "Jon Nicholson and Aidan Delaney",
title = "Formalising Simple Codecharts",
pages = "346--348",
booktitle = "7th International Conference on the Theory and Application of Diagrams",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
volume = "7352",
address = "Canterbury, UK",
month = "jul",
year = "2012",
doi = "10.1007/978-3-642-31223-6_47",
abstract = "Codecharts are a formal diagrammatic language for specifying the structure of object-oriented design patterns, frameworks, and programs. Codecharts are attractive for applications in both forward (e.g. design verification) and reverse engineering (e.g. program visualization). Although the definition of Codecharts has been adequate for these applications, there is a need to develop the language further in more precise terms. This paper outlines our work in refining the definition of Codecharts. We informally describe the concrete syntax and semantics of Codecharts, and provide a new formal abstract syntax. We conclude with a brief discussion on future work."
}

J. Nicholson, A. Delaney, and G. Stapleton, "Formalizing the syntax of codecharts," in 18th international conference on distributed multimedia systems, Miami Beach, FL, USA, 2012, pages 181-184.

[Notes] [BibTex]

BibTex

@inproceedings{nicholson_fsc_2,
author = "Jon Nicholson and Aidan Delaney and Gem Stapleton",
title = "Formalizing the Syntax of Codecharts",
pages = "181--184",
booktitle = "18th International Conference on Distributed Multimedia Systems",
publisher = "Knowledge Systems Institute",
address = "Miami Beach, FL, USA",
month = "aug",
year = "2012",
note = "Part of the 2012 International Workshop on Visual Languages and Computing (VLC2012)"
}

2011

J. Nicholson, "A theory of classes from the theoretical foundations of lepus3," in 13th international conference on formal engineering methods, Durham, UK, 2011, pages 522-536.

[Abstract] [BibTex]

BibTex

@inproceedings{nicholson_tctfl,
author = "Jonathan Nicholson",
title = "A Theory of Classes from the Theoretical Foundations of LePUS3",
booktitle = "13th International Conference on Formal Engineering Methods",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
volume = "6991",
address = "Durham, UK",
month = "oct",
year = "2011",
pages = "522--536",
doi = "10.1007/978-3-642-24559-6_35",
abstract = "LePUS3 is a formal design description language for specifying decidable (i.e. automatically verifiable) properties of object-oriented design. LePUS3 has been successfully applied to both design verification and reverse engineering applications. However, LePUS3 is becoming over zealously pragmatic. Its current definition is inflexible, limiting is expressivity, extensibility and reasoning capabilities. We present a new theory of classes derived from the theoretical foundations of LePUS3, and defined in the Typed Predicate Logic. The expressive power of our theory is demonstrated by specifying and reasoning over design patterns."
}

2009

J. Nicholson, E. Gasparis, A. H. Eden, and R. Kazman, "Automated verification of design patterns with lepus3," in 1st nasa formal methods symposium, Moffett Field, California, USA, 2009, pages 76-85.

[Abstract] [BibTex]

BibTex

@inproceedings{nicholson_avdpl,
author = "Jonathan Nicholson and Epameinondas Gasparis and Amnon H. Eden and Rick Kazman",
title = "Automated Verification of Design Patterns with LePUS3",
pages = "76--85",
booktitle = "1st NASA Formal Methods Symposium",
publisher = "NASA",
volume = "NASA/CP-2009-215407",
address = "Moffett Field, California, USA",
month = "apr",
year = "2009",
abstract = "Specification and [visual] modelling languages are expected to combine strong abstraction mechanisms with rigour, scalability, and parsimony. LePUS3 is a visual, object-oriented design description language axiomatized in a decidable subset of the first-order predicate logic. We demonstrate how LePUS3 is used to formally specify a structural design pattern and prove ( verify ) whether any JavaTM 1.4 program satisfies that specification. We also show how LePUS3 specifications (charts) are composed and how they are verified fully automatically in the Two-Tier Programming Toolkit."
}

2008

E. Gasparis, J. Nicholson, and A. H. Eden, "Lepus3: an object-oriented design description language," in 5th international conference on the theory and application of diagrams, 2008, pages 364-367.

[Abstract] [BibTex] [Link]

BibTex

@inproceedings{gasparis_looddl,
author = "Epameinondas Gasparis and Jonathan Nicholson and Amnon H. Eden",
title = "LePUS3: An Object-Oriented Design Description Language",
pages = "364--367",
booktitle = "5th International Conference on the Theory and Application of Diagrams",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
volume = "5223",
month = "sep",
year = "2008",
doi = "10.1007/978-3-540-87730-1_37",
url = "http://www.eden-study.org/articles/2008/lepus3-oo-design-description-lang.pdf",
abstract = "LePUS3 (lepus.org.uk) is a logic, visual, object-oriented Design Description Language: a formal specification language designed to capture and convey the building-blocks of object-oriented design. LePUS3 minimal vocabulary constitutes of abstraction mechanisms that can specify effectively and precisely design patterns and the design of JavaTM (C++, Smalltalk, etc.) programs at any level of abstraction."
}

E. Gasparis, A. H. Eden, J. Nicholson, and R. Kazman, "The design navigator: charting java programs," in 30th international conference on software engineering, Leipzig, Germany, 2008, pages 945-946.

[Abstract] [BibTex] [Link]

BibTex

@inproceedings{gasparis_dncjp,
author = "Epameinondas Gasparis and Amnon H. Eden and Jonathan Nicholson and Rick Kazman",
title = "The Design Navigator: Charting Java Programs",
pages = "945--946",
booktitle = "30th International Conference on Software Engineering",
publisher = "ACM",
address = "Leipzig, Germany",
month = "may",
year = "2008",
doi = "10.1145/1370175.1370200",
url = "http://www.eden-study.org/articles/2008/design-navigator-icse.pdf",
abstract = "The Design Navigator is a semi-automated design mining tool which reverse engineers LePUS3 design charts from JavaTM 1.4 programs at any level of abstraction in reasonable time. We demonstrate the Design Navigator's step-wise charting process of Java Foundation Classes, generating decreasingly abstract charts of java.awt and discovering building-blocks in its design."
}

E. Gasparis, J. Nicholson, A. H. Eden, and R. Kazman, "Navigating through the design of object-oriented programs," in Working conference on reverse engineering, Los Alamitos, CA, USA, 2008, pages 331-332.

[Abstract] [BibTex] [Link]

BibTex

@inproceedings{gasparis_ntdoop,
author = "Epameinondas Gasparis and Jonathan Nicholson and Amnon H. Eden and Rick Kazman",
title = "Navigating Through the Design of Object-Oriented Programs",
pages = "331--332",
booktitle = "Working Conference on Reverse Engineering",
publisher = "IEEE Computer Society",
address = "Los Alamitos, CA, USA",
year = "2008",
doi = "10.1109/WCRE.2008.41",
url = "http://www.eden-study.org/articles/2008/navigating-design-oop_wcre08.pdf",
abstract = "The design navigator is a tool for reverse-engineering object-oriented programs into charts at any level of abstraction. The design navigator discovers the object-oriented building blocks in the design of programs and visualises them in terms of LePUS3, a formal design description language. We demonstrate that program visualization in a formal language is not only possible in principle but also of practical benefit."
}

PhD Thesis

2011

J. Nicholson, "On the theoretical foundations of lepus3 and its application to object-oriented design verification," PhD Thesis, University of Essex, Colchester, UK, 2011.

[Notes] [BibTex]

BibTex

@phdthesis{nicholson_phd,
author = "Jonathan Nicholson",
title = "On the Theoretical Foundations of LePUS3 and its Application to Object-Oriented Design Verification",
school = "University of Essex",
address = "Colchester, UK",
year = "2011",
note = "Achieved pass. Supervised by Professor Raymond Turner and Dr Amnon H. Eden. Examined by Professor Martin Henson and Professor Jonathan P. Bowen"
}

Seminars

2017

J. Nicholson, (forthcoming) case study: think big, go global, Education Investor Global Conference, London, UK, October, 2017.

[BibTex]

2015

J. Nicholson, Querying ontologies with diagrams, Hastings Research Seminar, University of Brighton, UK, February, 2015.

[Notes] [BibTex]

BibTex

@misc{nicholson_qod,
author = "Jonathan Nicholson",
title = "Querying Ontologies with Diagrams",
publisher = "Hastings Research Seminar, University of Brighton, UK",
month = "February",
year = "2015",
note = "A seminar about my EPSRC First Grant proposal given to academics from multiple disciplines at the Hastings campus. Ultimately the grant proposal was rejected, but had some very positive feedback."
}

2014

J. Nicholson and S. Kapetanakis, Enhance your research and teaching with knowledge transfer, KTP Week, University of Brighton, UK, November, 2014.

[Notes] [BibTex]

BibTex

@misc{nicholson_ertkt,
author = "Jonathan Nicholson and Stelios Kapetanakis",
title = "Enhance your research and teaching with knowledge transfer",
publisher = "KTP Week, University of Brighton, UK",
month = "November",
year = "2014",
note = "A short presentation given as part of KTP Week at the University of Brighton in the Hastings Campus. The talk covered my experiences with the Colony101 project."
}

2013

J. Nicholson, Degrees in computing, University of Brighton, UK, September, 2013.

[Notes] [BibTex]

BibTex

@misc{nicholson_dc,
author = "Jonathan Nicholson",
title = "Degrees in Computing",
publisher = "University of Brighton, UK",
month = "September",
year = "2013",
note = "A short presentation given to year 12 college students at Bexhill 6th Form College (http://www.bexhillcollege.ac.uk/) as part of their University Progression Day. This talk was followed up by taster sessions in November of the same year. Although not related to my research or industry activities, I've included it here because I think it's a nice talk, the students responded to it well, and it may help other academics prepare similar talks."
}

2012

J. Nicholson, Modeling and visualizing object-oriented programs with codecharts, Hastings Research Seminar, University of Brighton, UK, November, 2012.

[Notes] [BibTex]

Technical reports

2007

J. Nicholson, A. H. Eden, and E. Gasparis, "Verification of lepus3/class-z specifications: sample models and abstract semantics for java 1.4," School of Computer Science and Electronic Engineering, University of Essex, UK, Technical Report CSM-471, ISSN 1744-8050, 2007.

[Abstract] [BibTex] [Link]

Abstract

This document is a compendium of examples that describe the entities and relations that represent the abstract semantics ( finite structures ) of programs in the JavaTM programming language. It is designed to provide further explanation to the definitions given in the LePUS3 and Class-Z Reference manual [Eden et al. 2007 ]. To remind the reader, a finite structure is a simplified ('abstracted') picture of the program, which 'flattens' the knotty structure and syntax of the source code into a set of primitive entities (also called entities of dimension 0 ) and relations. Essentially, each finite structure can be viewed as a relational database, or a set of tables which contain tuples of entities ('records'). Below we list a few sample Java programs and the finite structure that represents them.

BibTex

@techreport{nicholson_vlcssmasj14,
author = "Jonathan Nicholson and Amnon H. Eden and Epameinondas Gasparis",
title = "Verification of LePUS3/Class-Z Specifications: Sample models and Abstract Semantics for Java 1.4",
type = "Technical Report",
institution = "School of Computer Science and Electronic Engineering, University of Essex",
number = "CSM-471, ISSN 1744-8050",
address = "UK",
month = "dec",
year = "2007",
url = "http://lepus.org.uk/ref/verif/verif.pdf",
abstract = "This document is a compendium of examples that describe the entities and relations that represent the abstract semantics ( finite structures ) of programs in the JavaTM programming language. It is designed to provide further explanation to the definitions given in the LePUS3 and Class-Z Reference manual [Eden et al. 2007 ]. To remind the reader, a finite structure is a simplified ('abstracted') picture of the program, which 'flattens' the knotty structure and syntax of the source code into a set of primitive entities (also called entities of dimension 0 ) and relations. Essentially, each finite structure can be viewed as a relational database, or a set of tables which contain tuples of entities ('records'). Below we list a few sample Java programs and the finite structure that represents them."
}

A. H. Eden, E. Gasparis, and J. Nicholson, "Lepus3 and class-z reference manual," School of Computer Science and Electronic Engineering, University of Essex, UK, Technical Report CSM-474, ISSN 1744-8050, 2007.

[Abstract] [BibTex] [Link]

BibTex

@techreport{eden_lcrm,
author = "Amnon H. Eden and Epameinondas Gasparis and Jonathan Nicholson",
title = "LePUS3 and Class-Z Reference Manual",
type = "Technical Report",
institution = "School of Computer Science and Electronic Engineering, University of Essex",
number = "CSM-474, ISSN 1744-8050",
address = "UK",
month = "dec",
year = "2007",
url = "http://lepus.org.uk/ref/refman/refman.pdf",
abstract = "This document formally defines the elements in the syntax and the semantics of LePUS3 and the Class-Z specification languages. It was designed to satisfy the rigid requirements of mathematical logic, and it is therefore unsuitable for learning LePUS3 and Class-Z. To learn LePUS3 and Class-Z please see the Tutorial . To learn about the background and motivation see the About page. A legend offering a key to the language's symbols is also available."
}

A. H. Eden, E. Gasparis, and J. Nicholson, "The 'gang of four' companion: formal specification of design patterns in lepus3 and class-z," School of Computer Science and Electronic Engineering, University of Essex, UK, Technical Report CSM-472, ISSN 1744-8050, 2007.

[Abstract] [BibTex] [Link]

BibTex

@techreport{eden_gfcfsdplc,
author = "Amnon H. Eden and Epameinondas Gasparis and Jonathan Nicholson",
title = "The 'Gang of Four' Companion: Formal specification of design patterns in LePUS3 and Class-Z",
type = "Technical Report",
institution = "School of Computer Science and Electronic Engineering, University of Essex",
number = "CSM-472, ISSN 1744-8050",
address = "UK",
month = "dec",
year = "2007",
url = "http://lepus.org.uk/ref/companion/companion.pdf",
abstract = "This document demonstrates how the informal specifications of the design patterns the 'Gang of Four' seminal catalogue [Gamma et al 1995] can be specified formally using the LePUS3 and Class-Z Design Description Languages."
}

I use the Papercite plugin to display each publication with some tweaks.

Research Interests

I am interested in the fields of software engineering and knowledge representation. Of particular interest is developing novel visual languages with practical application that are more accessible than symbolic or textual notations.

Academic Esteem

I have acted as reviewer for international journals, including:

Innovations in Systems and Software Engineering
Formal Aspects of Computing
International Journal on Semantic Web and Information Systems (special issue on Visualisation of and Interaction with Semantic Web Data)
Journal of Visual Languages and Computing

I have acted as reviewer for several international conferences, including:

21st International Conference on Conceptual Structures (ICCS 2014)
21st IEEE International Conference on Web Services (ICWS 2014)
2nd IEEE International Conference on Mobile Services (MS 2013)
IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC 2012)

Awards & Recognition

Reading List of the Week - Talis Aspire, 29 April 2016
Excellence in Facilitating and Empowering Learning (nominated) - University of Brighton, April 2016
Excellence in Facilitating and Empowering Learning (nominated) - University of Brighton, April 2014
Fellow of the Higher Education Academy - November 2013
Best final year project prize. - University of Essex, July 2005

Dr Jon Nicholson

Experience

Industry

Research

Teaching

Qualifications

Publications

Journals

Books and book chapters

Conferences and workshops

PhD Thesis

Seminars

Technical reports

Research Interests

Academic Esteem

Awards & Recognition