Seminar Software Engineering - Topics '22

T1: Early validation of system requirements and design through BIP (black)

Early requirements validation aims to reduce the need for the high-cost validation testing and corrective measures at late development stages. Several approaches exist, such as the Behavior-Interaction-Priorities (BIP) component framework. BIP allows building complex designs by composing simpler reusable designs enforcing given properties. This seminar will give a brief tutorial of the use of BIP, highlighting the verification of the control software of the CubETH nanosatellite.

Stachtiari E, Mavridou A, Katsaros P, Bliudze S, Sifakis J. Early validation of system requirements and design through correctness-by-construction. J Syst Softw. 2018;145:52–78.

Basu, A., Bensalem, B., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J., 2011. Rigorous component-based system design using the bip framework. IEEE Softw. 28 (3), 41–48.

T2: Distributed Systems and TLA+ (red)

TLA+ is a specification language, used to design, model, document, and verify distributed systems, developed by Leslie Lamport (Turing Award 2013). A key feature of TLA+, is that it can be employed to uncover design flaws before system implementation is underway, as TLA+ specifications are amenable to model checking. The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desired properties such as safety and liveness. TLA+ is actively and successfully used in practice such as in Amazon AWS, or within critical distributed systems. This seminar will give an overview and a brief practical tutorial of TLA+.

Use of Formal Methods at Amazon Web Services: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf

https://pron.github.io/tlaplus

T3: FRET: Formal Requirements Elicitation and Reasoning (red)

FRET, developed at NASA Ames, is a framework for the elicitation, specification, formalization and understanding of requirements. Users enter system requirements in a specialized natural language, and FRET helps understanding and review of semantics by utilizing a variety of forms for each requirement: natural language description, formal mathematical logics, and diagrams. Requirements can be defined in a hierarchical fashion and can be exported in a variety of forms to be used by analysis tools. This seminar will give an overview of FRET, the way requirements are specified, reasoned upon and showcase the capabilities of the framework to interact with accompanying tools.

https://github.com/NASA-SW-VnV/fret

Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, Johann Schumann (2021). “Automated formalization of structured natural language requirements”. Information and Software Technology (IST) Journal, Special Section on REFSQ’20.

T4: Software Modeling with Alloy (green)

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. An Alloy model is a collection of constraints that describes (implicitly) a set of structures, for example: all the possible security configurations of a web application, or all the possible topologies of a switching network. Alloy’s tool, the Alloy Analyzer, is a solver that takes the constraints of a model and finds structures that satisfy them. Structures are displayed graphically, and their appearance can be customized for the domain at hand. This seminar will give an overview and walkthrough of Alloy.

http://alloytools.org/tutorials/day-course/

T5: Runtime Verification (blue)

Runtime verification (RV) is a lightweight verification technique based on observing information from a system while in operation, and identifying if the observed behaviors satisfy or violate certain properties. It has emerged as a practical application of formal verification, checking properties upon a sequence of events arising from system execution, thus scaling well in systems involving complex and high-throughput events. It is particularly useful when exhaustive design time verification is impractical or infeasible, or a system’s formal model is difficult to construct. Monitors are instead constructed from formal property specifications, which detect if an incoming event sequence violates them in an online manner. This seminar will focus on Metric Temporal Logic and Signal Temporal Logic with respect to their runtime verification. How a monitor is constructed, how a trace is checked, using a practical tool.

A brief account of runtime verification. Martin Leucker, Christian Schallhart

https://github.com/doganulus/reelay

https://arxiv.org/abs/1901.00175

T6: Satisfiability Modulo Theories (green)

Satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and various data structures. SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs, and have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing. This seminar will focus on practical SMT, where formulae are built programmatically, e.g., with python.

Leonardo de Moura and Nikolaj Bjørner. Satisfiability Modulo Theories: An Appetizer

https://github.com/pysmt/pysmt

T7: Explicit-state Model Checking (blue)

Model checking is a method for checking whether a finite-state model of a system meets a given specification. In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language. To this end, the problem is formulated as a task in logic, namely to check whether a structure satisfies a given logical formula. This general concept applies to many kinds of logic and many kinds of structures. This seminar will first study two fundamental logics (Computation Tree Logic and Linear Temporal Logic), their similarities and differences. Then, the focus will be on LTL, and how practical usage can be achieved with the SPOT tool, including automata and formula manipulation, model checking and tool interfacing.

Doron A. Peled, Edmund M. Clarke, and Orna Grumberg. Model Checking

https://spot.lrde.epita.fr/

T8: Probabilistic Model Checking with PRISM (green)

PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others. This seminar will give a tutorial on PRISM: its input language, support for underlying models, as well as practical usage.

Marta Kwiatkowska, Gethin Norman and David Parker. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV’11), volume 6806 of LNCS, pages 585-591, Springer, 2011.

https://www.prismmodelchecker.org/

T9: Monitoring Spatially-Distributed Systems with Spatio-Temporal Logics (red)

Runtime verification is a lightweight technique based on observing information from a system while in operation, and identifying if the observed behaviors satisfy or violate certain properties. Within the setting of mobile and also spatially distributed systems, monitoring is a central activity, making specification of spatio-temporal requirements and their verification essential. This seminar will present signal temporal logics (and perhaps their spatio-temporal extensions).

E. Bartocci, L. Bortolussi, M. Loreti, and L. Nenzi, “Monitoring mobile and spatially distributed cyber-physical systems,” in Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design. ACM, 2017, pp. 146–155.

H. Torfah, “Stream-based monitors for real-time properties,” in Intl. Conf. on Runtime Verification. Springer, 2019, pp. 91–110.

Ezio Bartocci, Luca Bortolussi, Laura Nenzi, Simone Silvetti: MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties.

T10: Feature Model Analysis with SAT (red)

Feature models are a compact representation of all the products of a software product line in terms of “features”. Feature models are commonly visually represented by means of feature diagrams, and are widely used during development process. The first goal of this seminar will be to represent a feature model programmatically using Satisfiability Modulo Theories (SMT), for example by making use of pysmt, javasmt etc. This will enable the second goal, which will be showing how the following two questions can be answered with such an SMT model: i) Given a partial configuration, which are options to produce valid configurations, and ii) How can conflicting (or dead) features of a feature model be detected.

https://github.com/pysmt/pysmt

D. Benavides, A.Ruiz-Cortés, P. Trinidad and S. Segura. “A Survey on the Automated Analyses of Feature Models” . Jornadas de Ingeniería del Software y Bases de Datos (JISBD'06). Sitges, Spain. 2006

Bürdek, J., Kehrer, T., Lochau, M. et al. Reasoning about product-line evolution using complex feature model differences. Autom Softw Eng 23, 687–733 (2016). https://doi.org/10.1007/s10515-015-0185-3

T11: Statistical Model Checking with Uppaal-SMC (blue)

Uppaal is a toolbox for verification of real-time systems represented by (a network of) timed automata extended with integer variables, structured data types, and channel synchronization. For this topic, a tutorial on Uppaal-SMC and its underlying timed automata models for hybrid and stochastic systems will be given, illustrating modeling features of the tool, usage of the graphical interface and of the simulation framework.

Uppaal SMC Tutorial, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen. International Journal on Software Tools for Technology Transfer (STTT), January 2015, Volume 17, Issue 4, pp 397-415. Springer Berlin Heidelberg.

https://uppaal.org/

T12: Software Model Checking with CBMC (black)

CBMC is a Bounded Model Checker for C and C++ programs. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. Furthermore, it can check C and C++ for consistency with other languages, such as Verilog. The verification is performed by unwinding the loops in the program and passing the resulting equation to a decision procedure. This seminar will focus on the verification of C programs, and give a practical tutorial on the capabilities and on how to apply CBMC.

http://www.cprover.org/cbmc/

T13: Software Model Checking C Source Code (black)

Software model checking is the algorithmic analysis of programs to prove properties of their executions. For this topic, an overview of the major techniques and tools (including bounded model checking, predicate abstraction, translations) will be given, with a focus on C source code.

https://link.springer.com/article/10.1007/s10009-009-0106-5

Software model checking. R Jhala, R Majumdar - ACM Computing Surveys (CSUR), 2009

T14: How do code documentation efforts spread over class hierarchy? (red)

Inheritance plays an essential role in object-oriented programming languages. It claims to aid in maintaining software, testing it, and producing high-quality software. As a class inherits another class, similarly documentation is also inherited in the subclasses. In Java, JavaDoc automatically inherits the superclass method’s comments in case there are no method comments provided for the overridden method. However, in practice, how deep the documentation hierarchy goes and how information is spread over different hierarchy levels is unknown. For example, In Pharo, 90% of root classes have longer comments than leaf classes. On the other hand, leaf classes can be documented by test cases, separate example class/methods, or examples in the comments.

Aim: To gather the information on how classes are documented, by class comments, method comments, test cases, or examples and design a visualization to present to the developers.

Research hypothesis: Leaf classes have more examples compared to root classes.

Steps:

  • Gather several projects in Java.
  • Gather information about how classes are documented.
  • Identify at which inheritance level classes are documented often.
  • Design a visualization to present the class documentation hierarchy.
  • Analyze the role of hierarchy in the class documentation.

“Reuse documentation and Documentation Reuse” by Semetinger “Evaluating Inheritance Depth on the Maintainability” by Daly et al., “How Documentation Evolves Over Time” by Schreck et al., “An Empirical Study of Evolution of Inheritance in Java OSS” by Nasseri et al.,

T15: The role of software documentation in Sustainable software engineering process (blue)

The software consists of various components, e.g., input, output, or supplement components. Given the increasing demand for software and rapid development of the software industry, researchers got confronted with the energy impact of software on the environment. Thus, they started to focus on measuring the energy consumption of current software and related software engineering processes to inform developers timely. Current research work in this direction has been limited to measuring the energy footprint of software using source code run time or compile time, computation power or storage power, etc., and very rarely on the supplement information. Since code comments are not compiled, they are rarely considered into such energy measurement tools.

Software documentation is an inexplicable part of the software. It helps developers in understanding and modifying the software in the development and maintenance phases. Code comments are an important type of software documentation and developers trust code comments more than other forms of documentation. However, what is the role of software documentation, particularly code documentation in greenware software development, how to measure their energy footprint, are yet unknown. To gain insights on these unknowns, we first need to understand and decompose the role of software documentation, and then accurately measure its energy impact. Such empirical understanding can help developers and researchers build or improve documentation tools to achieve overall sustainable software.

Research questions: What do developers understand by the term “Sustainable Software documentation” and what steps do they take to achieve it? To what extent, do current tools (measuring carbon footprints or energy consumptions) consider software documentation?

STEPS: Study the current literature in sustainable software engineering and identify how software documentation has been perceived and described in state-of-the-art. Conduct a survey to answer RQ1. Survey popular tools to answer RQ2.

Important papers to read: Systematic Mapping Study on Software Engineering for Sustainability (SE4S)—Protocol and Results Impacts of software and its engineering on the carbon footprint of ICT Measuring energy footprint of software features Calculating source line level energy information for Android applications Energy profiles of Java collections classes Mining Questions about Software Energy Consumption Labeling Sustainable Software Products and Websites: Ideas, Approaches, and Challenges An assessment of software lifecycle energy Agile practices for global software development vendors in the development of green and sustainable software

T16: Documentation practices of developers in Polyglot environments (red)

Introduction: Developers write various types of information in code comments such as a summary of the class, or a description of its methods and variables in comments. These information types help developers in understanding and modifying the code. However, developers follow different comment conventions to write various information in comments. In our previous work, we found instances of developers borrowing or carrying the style from other languages. for instance, we found developers writing instance variable or usage details in Java class comments where Java style guidelines do not suggest. Similarly, in Python and Smalltalk, we found developers writing Javadoc-style comments.

Such practices create a consistency problem (consistency of comments with style guideline conventions or project conventions). Current linters or recommendation projects address consistency problems without understanding the origin of practices. In this project, we want to understand to what extent such practices are prevalent. How can we recommend developer-specific practices?

STEPS:

  • Take popular, heterogeneous, big open source projects.
  • Identify three primary languages (Java, Python, C++)
  • Identify the primary developers of these languages.
  • Collect code comments of these developers in other languages.
  • Identify the influence of one programming language on other languages’ projects.
  • Compare their other languages project to the language style guidelines and see which kinds of commenting violations they often generate.
  • Learn common patterns of violated/adherence commenting practices of developers.
  • Develop a linter tailored to the background of a developer to handle such violations.
  • Evaluate the linter in the real setting.