Research Reports in Software Engineering and Management

Permanent URI for this collectionhttps://gupea-staging.ub.gu.se/handle/2077/24891

Software Engineering and Management is a research field which focuses on software processes, modelling, development, testing, requirements and quality assurance of software. This research report series is edited by the Software Engineering division at the department of Computer Science and Engineering.

Browse

Now showing 1 - 20 of 24

On the Specification and Monitoring of Timed Normative Systems
(2022) Azzopardi, Shaun; Pace, Gordon J.; Schapachnik, Fernando; Schneider, Gerardo
In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.
Runtime Verification of Kotlin Coroutines
(2022) Furian, Denis; Azzopardi, Shaun; Falcone, Yliès
Kotlin was introduced to Android as the recommended language for development. One of the unique functionalities of Kotlin is that of coroutines, which are lightweight tasks that can run concurrently inside threads. Programming using coroutines is difficult, among other things, because they can move between threads and behave unexpectedly. We introduce runtime verification in Kotlin. We provide a language to write properties and produce runtime monitors tailored to verify Kotlin coroutines. We identify, formalise and runtime verify seven properties about common runtime errors that are not easily identifiable by static analysis. To demonstrate the acceptability of the technique in real applications, we apply our framework to an in-house Android app and micro-benchmarks and measure the execution time and memory overheads.
AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification
(International Conference on Runtime Verification, 2022) Azzopardi, Shaun; Ellul, Joshua; Falzon, Ryan; Pace, Gordon J.
Aspect-oriented programming tools aim to provide increased code modularity by enabling programming of cross-cutting concerns separate from the main body of code. Since the inception of runtime verification, aspect-oriented programming has regularly been touted as a perfect accompanying tool, by allowing for non-invasive monitoring instrumentation techniques. In this paper we present, AspectSol, which enables aspect-oriented programming for smart contracts written in Solidity, and then discuss the design space for pointcuts and aspects in this context. We present and evaluate practical runtime verification uses and applications of the tool.
Tainting in Smart Contracts: Combining Static and Runtime Verification
(Lecture Notes in Computer Science book series (LNCS,volume 13498), 2022) Azzopardi, Shaun; Ellul, Joshua; Falzon, Ryan; Pace, Gordon J.
Smart contracts exist immutably on blockchains, making their pre-deployment correctness essential. Moreover, they exist openly on blockchains—open for interaction with any other smart contract and offchain entity. Interaction, for instance with off-chain oracles, can affect the state of the smart contract, and correctness of these smart contracts may depend on the trustworthiness of the data they manipulate or events they generate which, in turn, would depend on which parties or what information contributed to them. In this paper, we develop and present dynamic taint analysis techniques to enable data tainting in smart contracts. We propose an extension of Solidity that enables labelling inputs of interaction endpoints with dynamic data-carrying labels that capture actionable information about the sender. These labels can then be propagated dynamically across transactions to transitively dependent data. Specifications can then refer to such taints, for instance for ensuring that certain data could not have been influenced through interaction by a certain party. We further allow the use of taints as part of the language, affecting the control flow of the smart contract. To manage the overheads of such runtime tainting we develop sound static analysis-based techniques to prune away unnecessary instrumentation. We give a case study as a proof-of-concept, and measure the overheads associated with our additions before and after optimisation.
Model Checking Reconfigurable Interacting Systems
(International Symposium on Leveraging Applications of Formal Methods, 2022) Alrahman, Yehia Abd; Azzopardi, Shaun; Piterman, Nir
Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK (Find the associated toolkit repository here: https://github.com/dsynma/recipe.), to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, and self-organisation.
Runtime Verification meets Controller Synthesis
(2022) Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo
Reactive synthesis guarantees correct-by-construction controllers from logical specifications, but is costly—2EXPTIME-complete in the size of the specification. In a practical setting, the desired controllers need to interact with an environment, but the more precise the model of the environment used for synthesis, the greater the cost of synthesis. This can be avoided by using suitable abstractions of the environment, but this in turn requires appropriate techniques to mediate between controllers and the real environment. Runtime verification can help here, with monitors acting as these mediators, and even as activators or orchestrators of the desired controllers. In this paper we survey literature for combinations of monitors with controller synthesis, and consider other potential combinations as future research directions.
R-CHECK: A Model Checker for Verifying Reconfigurable MAS
(AAMAS 2022, 2022) Alrahman, Yehia Abd; Azzopardi, Shaun; Piterman, Nir
Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.
Incorporating Monitors in Reactive Synthesis without Paying the Price
(19th International Symposium on Automated Technology for Verification and Analysis, 2021) Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo
Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative speci cations, and have found languages that combine modelling with declarative speci - cations more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative speci cations in the presence of an existing behaviour model as a monitor, with the bene t of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeat- ing triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional syn- thesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we ap- ply it to speci cations requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametri- sation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.
Actions over Core-closed Knowledge Bases
(2022) Cauli, Claudia; Ortiz, Magdalena; Piterman, Nir
We present new results on the application of semantic- and knowledge-based reasoning techniques to the analysis of cloud deployments. In particular, to the security of Infrastructure as Code configuration files, encoded as description logic knowledge bases. We introduce an action language to model mutating actions; that is, actions that change the structural configuration of a given deployment by adding, modifying, or deleting resources. We mainly focus on two problems: the problem of determining whether the execution of an action, no matter the parameters passed to it, will not cause the violation of some security requirement (static verification), and the problem of finding sequences of actions that would lead the deployment to a state where (un)desirable properties are (not) satisfied (plan existence and plan synthesis). For all these problems, we provide definitions, complexity results, and decision procedures.
Proceedings of the 2nd edition of Swedish Workshop on the Engineering of Systems of Systems (SWESOS 2016)
(2017-09-30) Pelliccione, Patrizio; Bosch, Jan; Staron, Miroslaw; University of Gothenburg; Chalmers
Dashboard development guide How to build sustainable and useful dashboards to support software development and maintenance
(University of Gothenburg, 2015-11-24) Staron, Miroslaw; Torkar, Richard; University of Gothenburg
N/A
Ready for Prime Time, - Yes, Industrial-Grade Modelling Tools can be Used in Education
(University of Gothenburg, 2015-10-16) Liebel, Grischa; Heldal, Rogardt; Steghöfer, Jan-Philipp; Chaudron, Michel R V; Staron, Miroslaw; University of Gothenburg
It has been stated that industrial-grade modelling tools are unsuit- able for teaching modelling. In this paper, we present our experience with a university course on software modelling. In the first year of the course, we used a commercial modelling tool, in the second year the open- source alternative Papyrus. Both tools are considered to be of industrial grade and used in industry. Our quantitative analysis shows that the industrial-grade modelling tools with all their complexity did not have a negative impact on the students’ experience of modelling. This shows that industrial-grade modelling tools can be used in the classroom. We analyse why our experience differs from published accounts and conclude that the availability of a tool champion and tailored instruction mate- rial is key. From this, we derive recommendations for teacher support from tool-providers (vendors and open source), research directions for researchers and teachers, and for training efforts in the industry.
Report from the GI Dagstuhl Seminar 14433: Software engineering for Self-Adaptive Systems
(2014-10-24) Vogel, Thomas; Tichy, Matthias; Gorla, Alessandra; Staron, Miroslaw; Department of Computer Science and Engineering
Products and services such as business applications, vehicles, or devices in various domains such as transportation, communication, energy, production, or health. Consequently, our daily lives highly depend on such software-intensive systems. This results in complex systems, which is even more stressed by integrating them to systems-of-systems or cyber-physical systems such as smart cities. Therefore, innovative ways of developing, deploying, maintaining, and evolving such software-intensive systems are required. In this direction, one promising stream of software engineering research is self-adaptation. Engineering self-adaptive systems is an open research challenge, particularly, for software engineering since it is usually software that controls the self-adaptation. This GI-Dagstuhl seminar focused on software engineering aspects of building self-adaptive systems cost-effectively and in a systematic and predictable manner. This includes typical software engineering disciplines such as requirements engineering, modeling, architecture, middleware, design, analysis, testing, validation, and verification as well as software evolution.
Model-Based Engineering for Embedded Systems in Practice
(2014-11-18) Marko, Nadja; Liebel, Grischa; Sauter, Daniel; Lodwich, Aleksander; Tichy, Matthias; Leitner, Andrea; Hansson, Jörgen; Staron, Miroslaw; University of Gothenburg
Model-Based Engineering (MBE) aims at increasing the e↵ectiveness of engineering by using models as key artifacts in the development process. While empirical studies on the use and the e↵ects of MBE in industry generally exist, there is only little work targeting the embedded systems domain. We contribute to the body of knowledge with a study on the use and the assessment of MBE in that particular domain. Therefore, we collected quantitative data from 112 subjects, mostly professionals working with MBE, with the goal to assess the current State of Practice and the challenges the embedded systems domain is facing. Of the 112 subjects, the majority are experienced with MBE, working at large companies in the automotive, avionics, or healthcare domains. Additionally, mainly OEMs and First-tier suppliers are represented in the study. Our main findings are that MBE is used by a majority of all participants in the embedded systems domain, mainly for simulation, code generation, and documentation. Reported positive e↵ects of MBE are higher quality and improved reusability. Main shortcomings are interoperability difficulties between MBE tools, high training e↵ort for developers and usability issues. The data also shows that there are no large di↵erences between subgroups with respect to domains, position in the value chain, company size and product size.
Results from Two Controlled Experiments on the Effect of Using Requirement Diagrams on the Requirements Comprehension
(University of Gothenburg, 2013-04-02) Scanniello, Giuseppe; Staron, Miroslaw; Burden, Håkan; Heldal, Rogardt; Pareto, Lars; Universit a della Basilicata, Italy; Chalmers University of Technology; University of Gothenburg
We carried out a controlled experiment and an external replication to investigate whether the use of requirement diagrams of the SysML (System Modeling Language) helps in the comprehensibility of requirements. The original experiment was conducted at the University of Basilicata in Italy with Bachelor students, while its replication was executed at the University of Gothenburg in Sweden with Bachelor and Master students. A total of 87 participants took part in the two experiments. The achieved results indicated that the comprehension of requirements is statistically higher when requirements speci cation documents include requirement diagrams without any impact on the time to accomplish comprehension tasks.
A Light-Weight Defect Classification Scheme for Embedded Automotive Software Development
(2013-01-25) Mellegård, Niklas; Staron, Miroslaw; Törner, Fredrik; Chalmers University of Technology; University of Gothenburg; Volvo Car Corporation
Objective: Systematic software defect documentation is an essential part of software development process models as a means of early identification of patterns in defect inflow. Such documentation, however, may often be a tedious task requiring analysis work in addition to what is necessary to resolve the issue. Furthermore, generic defect documentation approaches often have a strong focus on source-code aspects making them unsuitable for development contexts with supplier-side implementation. To increase documentation efficiency in a development context with limited access to source-code, adapted schemes are needed. In this paper a light-weight defect classification scheme adapted to automotive software development is presented. Method: A case study was conducted at Volvo Car Corporation to adapt the IEEE Std. 1044 for the development of embedded automotive safety features. Results: The results consist of a detailed description of a defect classification scheme that complies with the IEEE Std. 1044. The main adaptations to the scheme consisted of raising the level of abstraction of the captured data items, shifting the focus from source-code to other artefacts and activities, and by conforming to the terminology of the company. Conclusions: We conclude that the IEEE Std. 1044 can be successfully adapted to a development context where source-code is not the main development artefact. Furthermore, initial evaluation showed that the adapted classification scheme captures what is currently tacit knowledge and has the potential of revealing patterns in the defects detected in different project phases. As a result we are currently in the process of incorporating the classification scheme into the company’s defect reporting system.
Proceedings of the 2nd Workshop on Experiences and Empirical Studies in Software Modelling
(2012-09-28) Chaudron, Michel; Genero, Marcela; Abrahão, Silvia; Pareto, Lars; Chalmers University of Technology and University of Gothenburg; University of Castilla-La Mancha; Universitat Politècnica de València
The International Workshop on Experiences and Empirical Studies in Software Modelling (EESSMod) is a satellite event of the ACM/IEEE International Conference on Model Driven Engineering Languages and Systems (MoDELS), with professionals and researchers interested in software modelling as intended audience, and with the bjective to 1) build a better understanding of the industrial use of modelling techniques, languages and tools; 2) start building theories about the effectiveness of modelling approaches; 3) identify directions for future research in the field; 4) facilitate and encourage joint research and experimentation in software modelling.The report contains the proceedings of the 2nd edition of the workshop, held in Innsbruck, Oct 2, 2012.
Towards Formalizing Assumptions on Architectural Level: A Proof-of-Concept
(Departmen of Computer Science and Engineering, 2012-09-10) Al Mamun, Abdullah; Tichy, Matthias; Hansson, Jörgen; Pareto, Lars; Chalmers | University of Gothenburg
While designing an architecture, architects often make assumptions about different factors like execution environment, structural properties of the artifacts, properties of input/output data etc. Implicit and invalid assumptions have been identified as a primary reason for architectural mismatches. Such mismatches cause nightmares to the people working at the system integration phase. Today’s complex systems operate in dynamic and rapidly changing environments. Implicit assumptions in the reusable components often make it challenging to adopt the components in a changed operational domain. If not documented, assumptions are often forgotten and it is both difficult and expensive to find them out from previously built software. This paper aims to formally capture assumptions at the architecture level so that they can be checked automatically throughout the system development. Automated checking of assumptions would facilitate a practicable assumption management system for complex and large-scale software system development with smooth integration and evolution.
Factors influencing reuse and speed in three organizations
(2012-05-29) Martini, Antonio; Lars, Pareto; Chalmers | University of Gothenburg
Architectural Concerns in Base Station Development
(Ericsson AB, 2010-12-17) Pareto, Lars; Dept. of Computer Science and Engineering at Chalmers | University of Gothenbyrg
This report presents a catalogue of architectural concerns found to be important to stakeholders within Ericsson’s Bases Station development. The catalogue is based on interviews with software architects, designers, testers, and team leaders within the software development organization of Ericsson’s W-CDMA base station development. It reflects concerns held by a representative sample of engineers (~1% of all project members), but is not a complete inventory of all concerns in base station development.

Browse

Recent Submissions