Distributed Ledger Technology (DLT), including blockchain, is increasingly used within industry ecosystems to create a high-integrity, single source of truth of shared data and business processes across diverse parties. A major challenge in adopting DLT is the conflicting demands on data transparency for improved integrity, against hiding commercially sensitive data. To address this, some industry ecosystems use multiple ledgers shared only between relevant parties rather than using a single distributed ledger across the entire ecosystem. The design problem for this is: What parties should share which ledgers, and what data should be on those ledgers? In this article, we propose a method employing a Design Structure Matrix (DSM) and Domain Mapping Matrix (DMM) to derive candidate shared ledger combinations for industry ecosystems. The method also indicates, for certain data, centralized web services or point-to-point messages may be more suitable than shared ledgers. We discuss our experiences with applying this method while developing a prototype for an agricultural traceability platform. We also present a genetic-algorithm-based DSM and DMM clustering technique to derive candidate shared ledger combinations.

The advent of Generative AI has marked a significant milestone in artificial intelligence, demonstrating remarkable capabilities in generating realistic images, texts, and data patterns. However, these advancements come with heightened concerns over data privacy and copyright infringement, primarily due to the reliance on vast datasets for model training. Traditional approaches like differential privacy, machine unlearning, and data poisoning only offer fragmented solutions to these complex issues. Our paper delves into the multifaceted challenges of privacy and copyright protection within the data lifecycle. We advocate for integrated approaches that combines technical innovation with ethical foresight, holistically addressing these concerns by investigating and devising solutions that are informed by the lifecycle perspective. This work aims to catalyze a broader discussion and inspire concerted efforts towards data privacy and copyright integrity in Generative AI.

Multi-party systems are important for business processes but can be complex. Blockchain facilitates trust in multi-party systems by providing transparency, decentralised control, and immutable transaction history, to improve security and accountability between parties. The use of cryptographic hashes and the continual validation of the shared ledger in a blockchain system provides parties with data integrity for historical transactions and process integrity for smart contract execution. However, in the design of a broader system combining a blockchain with off-chain components, it is not always clear how system-level integrity is supported. This paper proposes two modelling schemes to better understand blockchain's support for integrity in multi-party blockchain-based systems. The schemes model interactions between components in an architecture as security protocols, for analysis by standard techniques and tools. We first illustrate how blockchain-based systems can be abstractly modelled directly as security protocols. Then we show how blockchain-specific issues such as consensus-based ‘forking’ (also known as ‘orphan blocks’ or ‘uncle blocks’) can be encoded. This allows transaction reordering behaviour to manifest in the model, and allows design mitigation for that problem to be checked. We illustrate our approach with analyses of three design alternatives for possible enhancements to a multi-party system for sharing trade certificates.

Abstract Blockchain has attracted broad interests to build decentralised applications. A typical class of applications uses blockchain for the management of cross‐organisational business processes as well as assets. However, developing such applications without introducing vulnerabilities is hard for developers, not the least because the deployed code is immutable and can be called by anyone with access to the network. Model‐driven engineering (MDE) helps to reduce those risks, by combining proven code snippets as per the model specification, which is easier to understand than source code. Therefore, in this article, we present an approach for integrated MDE across business processes and asset management (e.g., for settlement). Our approach includes methods for fungible/non‐fungible asset registration, escrow for conditional payment, and asset swap. The proposed MDE approach is implemented in a smart contract generation tool called Lorikeet, and evaluated in terms of feasibility, functional correctness, and cost effectiveness.

Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the Ethereum Virtual Machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions in relationships between parties. Smart contracts can carry financial value, and are increasingly used for safety-, security-, or mission-critical purposes. Errors in smart contracts have led and will lead to loss or harm. Formal verification can provide the highest level of confidence about the correct behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. We structure bytecode sequences into blocks of straight-line code and create a program logic to reason about these. This abstraction is a step towards control of the cost and complexity of formal verification of EVM smart contracts.

Privacy-preserving data analytics is an emerging technology which allows multiple parties to perform joint data analytics without disclosing source data to each other or a trusted third-party. A variety of platforms and protocols have been proposed in this domain. However, these systems are not yet widely used, and little is known about them from a software architecture and performance perspective. Here we investigate the feasibility of using architectural performance modelling and simulation tools for predicting the performance of privacy-preserving data analytics systems. We report on a lab-based experimental study of a privacy-preserving credit scoring application that uses an implementation of a partial homomorphic encryption scheme. The main experiments are on the impact of analytic problem size (number of data items and number of features), and cryptographic key length for the overall system performance. Our modelling approach performed with a relative error consistently under 5\% when predicting the median learning time for the scoring application. We find that the use of this approach is feasible in this technology domain, and discuss how it can support architectural decision making on trade-offs between properties such as performance, cost, and security. We expect this to enable the evaluation and optimisation of privacy-preserving data analytics technologies.

Blockchain is of rising importance as a technology for engineering applications in cross-organizational settings, avoiding reliance on central trusted third-parties. The use of blockchain, instead of traditional databases or services, is an architectural choice in the development of a software system. The costs of execution and storage are important non-functional qualities, but as yet very little has been done to study them for blockchain-based systems. We investigate the cost of using blockchain using business process execution as a lens. Specifically, we compare the cost for computation and storage of business process execution on blockchain vs. a popular cloud service. First, we capture the cost models for both alternatives. Second, we implemented and measured the cost of business process execution on blockchain and cloud services for an example business process model from the literature. We observe two orders of magnitude difference in this cost.

Blockchain is an emerging technology for decentralised and transactional data sharing across a large network of untrusted participants. It enables new forms of distributed software architectures, where agreement on shared states can be established without trusting a central integration point. A major difficulty for architects designing applications based on blockchain is that the technology has many configurations and variants. Since blockchains are at an early stage, there is little product data or reliable technology evaluation available to compare different blockchains. In this paper, we propose how to classify and compare blockchains and blockchain-based systems to assist with the design and assessment of their impact on software architectures. Our taxonomy captures major architectural characteristics of blockchains and the impact of their principal design decisions. This taxonomy is intended to help with important architectural considerations about the performance and quality attributes of blockchain-based systems.

Blockchain is an emerging technology for sharing transactional data and computation without using a central trusted third party. It is an architectural choice to use a blockchain instead of traditional databases or protocols, and this creates trade-offs between non-functional requirements such as performance, cost, and security. However, little is known about predicting the behaviour of blockchain-based systems. This paper shows the feasibility of using architectural performance modelling and simulation tools to predict the latency of blockchain-based systems. We use established tools and techniques, but explore new blockchain-specific issues such as the configuration of the number of confirmation blocks and inter-block times. We report on a lab-based experimental study using an incident management system, showing predictions of median system level response time with a relative error mostly under 10%. We discuss how the approach can be used to support architectural decision-making, during the design of blockchain-based systems.

Blockchain has recently gained momentum. Startups, enterprises, banks, and government agencies around the world are exploring the use of blockchain for broad applications including public registries, supply chains, health records, and voting. Dependability properties, like availability, are critical for many of these applications, but the guarantees offered by the blockchain technology remain unclear, especially from an application perspective. In this paper, we identify the availability limitations of two mainstream blockchains, Ethereum and Bitcoin. We demonstrate that while read availability of blockchains is typically high, write availability - for transaction management - is actually low. For Ethereum, we collected 6 million transactions over a period of 97 days. First, we measured the time for transactions to commit as required by the applications. Second, we observed that some transactions never commit, due to the inherent blockchain design. Third and perhaps even more dramatically, we identify the consequences of the lack of built-in options for explicit abort or retry that can maintain the application in an uncertain state, where transactions remain pending (neither aborted nor committed) for an unknown duration. Finally we propose techniques to mitigate the availability limitations of existing blockchains, and experimentally test the efficacy of these techniques.

Formal verification can provide the highest degree of software assurance. Demand for it is growing, but there are still few projects that have successfully applied it to sizeable, real-world systems. This lack of experience makes it hard to predict the size, effort and duration of verification projects. In this paper, we aim to better understand possible leading indicators of proof size. We present an empirical analysis of proofs from the landmark formal verification of the seL4 microkernel and the two largest software verification proof developments in the Archive of Formal Proofs. Together, these comprise 15,018 individual lemmas and approximately 215,000 lines of proof script. We find a consistent quadratic relationship between the size of the formal statement of a property, and the final size of its formal proof in the interactive theorem prover Isabelle. Combined with our prior work, which has indicated that there is a strong linear relationship between proof effort and proof size, these results pave the way for effort estimation models to support the management of large-scale formal verification projects.

Context: Recent projects such as L4.verified (the verification of the seL4 microkernel) have demonstrated that large-scale formal program verification is now becoming practical.

Size and effort estimation is a significant challenge for the management of large-scale formal verification projects. We report on an initial study of relationships between the sizes of artefacts from the development of seL4, a formally-verified embedded systems microkernel. For each API function we first determined its COSMIC Function Point (CFP) count (based on the seL4 user manual), then sliced the formal specifications and source code, and performed a normalised line count on these artefact slices. We found strong and significant relationships between the sizes of the artefact slices, but no significant relationships between them and the CFP counts. Our finding that CFP is poorly correlated with lines of code is based on just one system, but is largely consistent with prior literature. We find CFP is also poorly correlated with the size of formal specifications. Nonetheless, lines of formal specification correlate with lines of source code, and this may provide a basis for size prediction in future formal verification projects. In future work we will investigate proof sizing.

Background- Risks associated with a software project have the potential to affect all stakeholders. Today much software makes use of off-the-shelf (OTS) components. A better understanding of OTS-derived software risks will help to define responsibilities for these risks, and also to avoid them. Aim- Our objective is to identify, classify and compare risks of OTS-based software projects from both a software development and a software acquisition perspective. Method- To identify and classify the risks, we performed a systematic mapping study. In order to compare risks of OTS-based software development and acquisition in the real world setting, we used the mapping study results to survey occurrences of 11 shared risks in OTS-based software, in 35 OTS-based software developments and 34 OT-Sbased software acquisitions of Indonesian background. The survey is a partial replication of a previous study. Results- We identified 133 risks associated with OTS-based software development and 36 risks associated with OTS-based software acquisition. These risks are grouped into 17 risk categories. Risks occurred more frequently in software acquisition than in software development. In addition, two risks, insufficient OTS component documents and lack of provider technical support and training, frequently occurred only in the software development. Conclusions- In OTS-based projects, most risks for acquisition and development are similar. Technical-related risks are found less often in acquisition and project management related risks are found less often in development. Shared risks are perceived differently by developers and acquirers. Better understanding of actual and perceived risk in OTS-based software projects will improve risk management. Further work to validate these results is ongoing.

Project stakeholders can have different perceptions of risks and how they should be mitigated, but these differences are not always well understood and managed. This general issue occurs in Off-the-shelf (OTS)-based custom software development projects, which use and integrate OTS software in the development of specialized software for an individual customer. We report on a study of risk perceptions for developers and acquirers in OTS-based custom software development projects. The study used an online questionnaire-based survey. We compared stakeholders' perceptions about their level of control over and exposure to 11 shared risks in OTS-based software, in 35 OTS-based software developments and 34 OTS-based software acquisitions of Indonesian background. We found that both stakeholders can best control, and are most impacted by, risks about requirements negotiation. In general stakeholders agree who can best control risks (usually the developer), but there were different perceptions about who is most impacted by risks (the developer reported either themselves or both stakeholders; while usually the acquirer reported both stakeholders). In addition, both stakeholders agree that the acquirer is most impacted by the risk of reduced control of future evolution of the system. We also found disagreement about who is most impacted by the risk of lack of support (usually each stakeholder reported themselves). This paper makes two main contributions. First, the paper presents a method based on stakeholder analysis to compare perceptions of the respondents about which stakeholder is affected by and can control risks. Second, knowing stakeholder agreement on which stakeholder has high risk control should be helpful to rationalize responsibility for risks.

The L4.verified project was a rare success in large-scale, formal verification: it provided a formal, machine-checked, code-level proof of the full functional correctness of the seL4 microkernel. In this paper we report on the development process and management issues of this project, highlighting key success factors. We formulate a detailed descriptive model of its middle-out development process, and analyze the evolution and dependencies of code and proof artifacts. We compare our key findings on verification and re-verification with insights from other verification efforts in the literature. Our analysis of the project is based on complete access to project logs, meeting notes, and version control data over its entire history, including its long-term, ongoing maintenance phase. The aim of this work is to aid understanding of how to successfully run large-scale formal software verification projects.

The L4.verified project successfully completed a large-scale machine-checked formal verification at the code level of the functional correctness of the seL4 operating system microkernel. The project applied a middle-out process, which is significantly different from conventional software development processes. This paper reports a simulation model of this process; it is the first simulation model of a formal verification process. The model aims to support further understanding and investigation of the dynamic characteristics of the process and to support planning and optimization of future process enactment. We based the simulation model on a descriptive process model and information from project logs, meeting notes, and version control data over the project's history. Simulation results from the initial version of the model show the impact of complex coupling among the activities and artifacts, and frequent parallel as well as iterative work during execution. We examine some possible improvements on the formal verification process in light of the simulation results.

Many companies use Global Software Development (GSD) to access skilled people, reduce costs and utilize around the clock development. GSD has numerous social and technical difficulties, but most literature only examines social difficulties. Few studies concern technical difficulties or address Software Configuration Management (SCM) issues. SCM is widely used, and supports the infrastructure and practices that enable change management and version control. SCM has potential to support more effective GSD, but is more difficult in GSD, because coordination and synchronization are more complex. This paper presents our findings of a systematic mapping study of SCM in GSD. Systematic mapping is a methodology to discover and categorize research on a topic, and can be used to identify common themes and areas requiring further study. We find most research on SCM in GSD has used case studies, and there has been little empirical validation. The lack of coordination and group awareness causes difficulties for SCM in GSD, but no SCM process has been proposed to address this. More research is required on Software Configuration Control for GSD.

REpresentational State Transfer (REST) is the set of design principles behind the World Wide Web (WWW). REST treats all entities in the world as link-connected resources, and supports a resource-oriented architecture (ROA) for the design of applications. REST and ROA are responsible for many of the desirable quality attributes achieved in the WWW, such as loose-coupling (better adaptability) and interoperability. However, many exiting Web-based or service-oriented applications (WSDL/SOAP-based) only use WWW/HTTP as a tunneling protocol or abuse URL and POX (Plain Old XML) by encoding method semantics in them. These applications use fine-grained remote procedure calls (RPC), breaking REST/ROA principles. We observe two kinds of challenges: 1) conceptually modelling process-intensive applications using a ROA promoted by the REST principles; and 2) practically decomposing a workflow-based business process into distributed, dynamic and RESTful process fragments. In this paper, we propose a ROA for business processes following the RESTful principles. We evaluate our approach by comparing it with current SOAP/WSDL/BPEL-driven approaches in terms of feasibility, process visibility, interoperability, and adaptability.

Many industries have been developing e-business standards to improve business-to-business interoperability on a mass scale. Most such standards are composed of business data models with some message exchange patterns. Such data-only standards leave a very large interpretation space for the implementation stage at each individual organization. Thus, true industry-wide interoperability is still hard to achieve. In this industry report, we describe our experiences in creating and evaluating reference architectures for the Australian lending industry. To achieve the right level of prescriptiveness, our reference architectures are deliberately non-structural. Instead, they are based on a set of quality-centric architectural rules. We devised new methods for analyzing interoperability and evaluating such industry-level reference architectures. The first reference architecture has now been adopted and achieved positive effects. We also summarize several other lessons we learned, such as the need to align reference architectures with industry structures.

A systematic review is a defined and methodical way to identify, assess and analyse published primary studies in order to investigate a specific research question. Kitchenham has recently published guidelines for software engineering researchers performing systematic reviews. The objective of our paper is to critique Kitchenham’s guidelines and to comment on systematic review generally with respect to our experiences conducting our first systematic review. Our perspective as neophytes may be particularly illuminating for other software engineering researchers who are also considering conducting their first systematic review. Overall we can recommend Kitchenham’s guidelines to other researchers considering systematic reviews. We caution researchers to clearly and narrowly define the research questions they will investigate by systematic review, to reduce the overall effort and to improve the quality of the selection of papers and extraction of data. In particular we recommend defining complementary research questions that are not within the scope of the systematic review in order to clarify the boundaries of the specific research question of interest. An instance of this recommendation is that researchers should clearly define the unit of study for the systematic review.

Product line software engineering (PLSE) has proved to be an effective way to benefit from code reuse, leading to improved development efficiency, time-to-market, and product quality. In PLSE, a set of related products is developed by combining reused core assets with product-specific custom assets. Core assets implement most product functionality, and support variable functionality. Custom assets integrate a product's core assets, instantiate variation points, and implement functionality unique to the product. PLSE poses challenges for change control. Software engineering change control is related to configuration management (CM), and is concerned with planning, coordinating, tracking, and managing the impact of change to software artifacts (e.g. source code). The root cause of change control problems for PLSE is that core assets are shared between products that have different stakeholders. Core assets must satisfy the sometimes conflicting needs of these stakeholders. This position paper lists some specific change control problems characteristic of, or exacerbated by, PLSE and some of their solutions. These were observed during the author's prior experience working in a company that adopted PLSE and maintained product lines.

Many organizations used software product line development to improve development efficiency, time-to-market, and product quality. However, a perceived barrier to entry for product line development is that a product line architecture is required to handle variation across the product set. We describe qualitative evidence from industrial experiences with an approach that has allowed the adoption of product line development for a pre-existing product set, without the use of a product line architecture. The approach relies on file-level reuse and variation mechanisms provided by a configuration management infrastructure. The approach can reduce the risks and up-front costs of adopting product line development. Although not requiring a product line architecture, the approach is not inconsistent with architectural-level variation mechanisms. It has allowed previously-reported "reactive? and "proactive" styles of architectural evolution to support variation, and also a new "retroactive" style of architectural evolution. Additionally, the approach has provided new options for "working around" change control conflicts on reused product line core assets.

Abstract. This paper presents novel definitions of interfaced recursion blocks, interfaced procedures, and interfaced recursive procedures for the Refinement Calculus. These definitions allow step-wise refinement rules to be formally stated and proved for these constructs. An interface is associated with a (recursive) call by preceding the body of the implementation by an assertion statement which says that the interface refines to the implementation. An interface will typically be a specification statement, but in principle can be any command. The theory and rules presented in this paper have been mechanised in the theorem prover Isabelle/ZF.

August 01 1996 Using Bottlenecks in Feedforward Networks as a Dimension Reduction Technique: An Application to Optimization Tasks In Special Collection: CogNet Janet Wiles, Janet Wiles Departments of Computer Science and Psychology, The University of Queensland, Queensland 4072, Australia Search for other works by this author on: This Site Google Scholar Paul Bakker, Paul Bakker Departments of Computer Science and Psychology, The University of Queensland, Queensland 4072, Australia Search for other works by this author on: This Site Google Scholar Adam Lynton, Adam Lynton Department of Computer Science, The University of Queensland, Queensland 4072, Australia Search for other works by this author on: This Site Google Scholar Michael Norris, Michael Norris Department of Computer Science, The University of Queensland, Queensland 4072, Australia Search for other works by this author on: This Site Google Scholar Sean Parkinson, Sean Parkinson Department of Computer Science, The University of Queensland, Queensland 4072, Australia Search for other works by this author on: This Site Google Scholar Mark Staples, Mark Staples Department of Computer Science, The University of Queensland, Queensland 4072, Australia Search for other works by this author on: This Site Google Scholar Alan Whiteside Alan Whiteside Department of Computer Science, The University of Queensland, Queensland 4072, Australia Search for other works by this author on: This Site Google Scholar Author and Article Information Janet Wiles Departments of Computer Science and Psychology, The University of Queensland, Queensland 4072, Australia Paul Bakker Departments of Computer Science and Psychology, The University of Queensland, Queensland 4072, Australia Adam Lynton Department of Computer Science, The University of Queensland, Queensland 4072, Australia Michael Norris Department of Computer Science, The University of Queensland, Queensland 4072, Australia Sean Parkinson Department of Computer Science, The University of Queensland, Queensland 4072, Australia Mark Staples Department of Computer Science, The University of Queensland, Queensland 4072, Australia Alan Whiteside Department of Computer Science, The University of Queensland, Queensland 4072, Australia Received: December 13 1993 Accepted: January 22 1996 Online ISSN: 1530-888X Print ISSN: 0899-7667 © 1996 Massachusetts Institute of Technology1996 Neural Computation (1996) 8 (6): 1179–1183. https://doi.org/10.1162/neco.1996.8.6.1179 Article history Received: December 13 1993 Accepted: January 22 1996 Cite Icon Cite Permissions Share Icon Share Facebook Twitter LinkedIn Email Views Icon Views Article contents Figures & tables Video Audio Supplementary Data Peer Review Search Site Citation Janet Wiles, Paul Bakker, Adam Lynton, Michael Norris, Sean Parkinson, Mark Staples, Alan Whiteside; Using Bottlenecks in Feedforward Networks as a Dimension Reduction Technique: An Application to Optimization Tasks. Neural Comput 1996; 8 (6): 1179–1183. doi: https://doi.org/10.1162/neco.1996.8.6.1179 Download citation file: Ris (Zotero) Reference Manager EasyBib Bookends Mendeley Papers EndNote RefWorks BibTex toolbar search Search Dropdown Menu toolbar search search input Search input auto suggest filter your search All ContentAll JournalsNeural Computation Search Advanced Search © 1996 Massachusetts Institute of Technology1996 Article PDF first page preview Close Modal You do not currently have access to this content.