Publications

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."
}

2011

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

[BibTex] [Link]

2017

J. Nicholson and I. Tasker, “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.

[Abstract] [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."
}

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"
}

Publications

Publications

/What I’ve written

Journals

Books and book chapters

Conferences and workshops

PhD Thesis