The DesignDAO is a concept of planning, conducting and auditing Human-Centered Design (HCD) through a Decentralized Autonomous Organization (DAO). Human-Centered Design is commonly executed by multidisciplinary teams of skilled experts in the fields of psychology, design and IT amongst others. The activities of HCD – process planning, context analysis, requirements engineering, prototyping and evaluation – result in several defined work packages for each project. Each work package requires a certain mix of skills, found in different individuals. A DAO distributes decision-making, management, and entity ownership amongst the organization’s community. The concept of the DesignDAO describes how HCD work packages can get organized, managed and controlled in a decentralized, autonomous fashion.
This paper presents a preliminary exploration of the design and deployment of solidarity primitives for web3 social security, based on the insights generated during Other Internet’s Web3 Work Forum held in July 2023. The paper proposes a modular framework to develop solidarity primitives addressing the three dimensions of security for DAO contributors: psychosocial stability, financial stability and regulatory clarity. Additionally, it outlines a range of both on-chain and off-chain mechanisms and improvement proposals specific to each dimension. Lastly, it discusses current challenges to implementation.
The Blockchain 2.0 era integrated with smart contract along with its platforms and applications have experienced explosive growth in recent years. However, many smart contracts deployed in practice are prone to errors and cannot be modified due to the immutability of the blockchain. In light of this, it is vital to ensure the security of correctness of smart contracts before deployment. This paper proposes a formal modeling method based on Timed Colored Petri net (TCPN) to anlyze smart contracts with time constrains. We apply this formalism to a concrete voting contract system. Its functional requirements are formalized by the improved computing timing logic ASK-CTL with ML (Meta Language). Simulation and experiment show that the security and reliability of the voting contract can be effectively guaranteed.
Research on blockchains addresses multiple issues, with one being the automated creation of smart contracts. Developing smart contract methods is more difficult than mainstream software development as the underlying blockchain infrastructure poses additional complexity. We report on a new approach to developing smart contracts with the objective of automating the process to increase developer efficiency and reduce the risk of errors introduced by software developers. To support industry adoption, we use Business Process Model and Notation (BPMN) modeling to describe an application while targeting applications in the trade vertical. We describe a system that transforms a BPMN model into a multi-modal model that combines Discrete Event (DE) modeling for concurrency with Hierarchical State Machines (HSMs) to represent application functionality. Then, further transformations are used to transform the DE-HSM model into methods in smart contracts. The system lets the modeler decide which of the independent patterns should be transformed into methods of a separate smart contract that is deployed on a sidechain for the purpose of (i) reducing processing costs and/or (ii) providing privacy so that other participants in the smart contract do not have visibility into the processing of the pattern. We also briefly describe a proof-of-concept tool we built to demonstrate the feasibility of our approach.
Abstract Business Processes (BPs) are commonly used by organizations to describe their goals. However, the existent decentralization found in many organizations forces them to build such BPs by coordinating distributed and fragmented BPs. Within this context, microservices arise as a very interesting and convenient way to address the implementation of such processes due to their low coupling characteristic. In this case, the coordination of such fragmented BPs is usually achieved by means of event-based choreographies. One of the main challenges to be faced by choreographies is their evolution due to the complexity that introduces the need of integrating changes among autonomous and independent partners. We face the challenge of evolving a microservice composition that is globally defined in a BPMN model but executed through a choreography of BPMN fragments. We introduce a protocol to manage the propagation of a change done by one microservice to be integrated into both the BPMN fragments of the rest of the microservices and the global BPMN model. This protocol also supports the negotiation among participants and the automatic suggestion of model adaptations to maintain the functional integrity of the composition. These suggestions are supported by a catalogue of adaptation rules that precisely characterize every possible change and propose actions to be considered by the affected microservices. All the evolution process is done at the modelling level, without managing hard-coded implementations. We have developed specific tools to facilitate the practical adoption of this protocol, and we have validated our work in an experiment with users. We can conclude that the proposed approach is effective to evolve microservice compositions implemented as event-based choreography of BPMN fragments from the local perspective of one partner.
Luciano Baresi, Giovanni Quattrocchi, Damian A. Tamburri, Luca Terracciano
The deployment and management of Blockchain applications require non-trivial efforts given the unique characteristics of their infrastructure (i.e., immutability) and the complexity of the software systems being executed. The operation of Blockchain applications is still based on ad-hoc solutions that are error-prone, difficult to maintain and evolve, and do not manage their interactions with other infrastructures (e.g., a Cloud backend). This paper proposes KATENA, a framework for the deployment and management of Blockchain applications. In particular, it focuses on applications that are compatible with Ethereum, a popular general-purpose Blockchain technology. KATENA provides i) a metamodel for defining Blockchain applications, ii) a set of processes to automate the deployment and management of defined models, and iii) an implementation of the approach based on TOSCA, a standard language for Infrastructure-as-Code, and xOpera, a TOSCA-compatible orchestrator. To evaluate the approach, we applied KATENA to model and deploy three real-world Blockchain applications, and showed that our solution reduces the amount of code required for their operations up to $82.7\%$.
Research on blockchains addresses multiple issues, with one being automating creation of smart contracts. One of the promising approaches, targeted for industry adoption, uses Business Process Model and Notation (BPMN) modeling to describe an application that is transformed into a smart contract. Although systems using this approach have been developed as a proof of concept, they do not address a major issue arising in the trade vertical that has applications involving collaboration of many actors over a long period of time. There are two difficulties: (i) BPMN's concept of a transaction is limited to actions of one actor, while trade transactions involve collaborations by many actors, and (ii) trade applications are long term and thus require support of transactional activities that span invocations of several methods of a smart contract. The difficulty is that a blockchain infrastructure supports the transactional properties only within the scope of one execution of one method of a smart contract. We extend the BPMN model by introducing the concept of a collaborative transaction to represent activities of many actors. In our previous research, we developed an approach, and a tool as a proof of concept, to transform a BPMN model into methods of a smart contract. In this paper we describe how collaborative transactions are supported by our approach even though the transaction activities span multiple calls to methods of a smart contract produced by transformation from a BPMN model to methods of a smart contract.
G V Sudharmendra, Bhuvenashwer Swaroop, L M Gokul, B Vineetha · 5 authors
Decentralized applications have evolved in the recent past. Many sectors have shown focus towards the Decentralized applications. This paper extends the application to the education sector. The work is associated with the creation of a Decentralized Application on the Ethereum Blockchain, which includes the decentralized way of storing data such as the student details. Face detection feature has been incorporated to tackle the problem of proxy attendance and other malpractices. The Decentralized Application interacts with the smart contract written on the Ethereum network. The smart contract created involves in storing the details of the student’s education timeline, such as his/ her marks, institution information, etc. Cloud technology has been used to store large files which cannot be stored in the smart contracts. Many natural calamities and other causes have led to the destruction of the stored details in the traditional databases, these problems have been overcome with this use of Cloud technology, where it provides features like replicability to avoid loses, reliability to avoid failures, scalability to avoid shortage of resources, etc. Authentication has been addressed with the help of face recognition tool which detects the identity of a person. This attempt of solving the above problems have been stated in this paper. Addition of a security layer with face recognition, storage of media files in the AWS S3 cloud, and interaction with the Decentralized Application, makes this paper unique from the other papers.
Norine Coenen, Bernd Finkbeiner, Jana Hofmann, Julia Tillman
Smart contracts are small but highly security-critical programs that implement wallets, token systems, auctions, crowd funding systems, elections, and other multi-party transactions on the blockchain. A broad range of methods has been developed to ensure that a smart contract is functionally correct. However, smart contracts often additionally need to satisfy certain hyperproperties, such as symmetry, determinism, or an information flow policy. In this paper, we show how a synthesis method for smart contracts can ensure that the contract satisfies its desired hyperproperties. We build on top of a recently developed synthesis approach from specifications in the temporal logic TSL. We present HyperTSL, an extension of TSL for the specification of hyperproperties of infinite-state software. As a preprocessing step, we show how to detect if a hyperproperty has an equivalent formulation as a (simpler) trace property. Finally, we describe how to refine a synthesized contract to adhere to its HyperTSL specification.
Blockchain represents a trusted source of data for process mining where the benefit is mutual since process mining provides blockchain applications with helpful insights on user behavior, performance and security. However, blockchain data is not adequate for process mining and this issue has been studied in several works. The focus of existing works was on extracting event logs from activity-centric applications, excluding blockchain artifact-centric applications which are more common. To address this limitation, we propose an approach for extracting blockchain data from artifact-centric applications in a format that is suitable for process mining techniques. To do so, we introduce ACEL (Artifact-Centric Event Logs), an extension of the OCEL (Object-Centric Event Logs) standard for artifact-centric processes. We also propose an algorithm to extract ACEL logs from Ethereum, a blockchain platform. We implemented the approach and compared its results with related standards using as case study a popular Ethereum decentralized application.
The analysis of existing research in the field of business processes automation is carried out. Modern business process automation methods involve the direct developers participation. Our proposed approach will allow domain experts to develop and manage smart contracts for business processes without the help of programmers. The methods of automating the smart contracts creation using semantic modeling are described. Methods of automation of complex processes with hierarchical nesting are proposed. A methodological approach to automating the smart contracts development using situation models is described. The operation scheme of the software system for the business processes formalization by constructing situation models is presented. The use of predicates ontological homomorphism to create smart contract templates is described. Methods of generating smart contracts in the sDSL language based on the described partial models are proposed. Examples of translating the business processes representation using situation models into smart contracts in the sDSL language are given. The interaction of several smart contracts using situation models with each other is described.
The formal description and verification of networks of cooperative and interacting agents is made difficult by the interplay of several different behavioral patterns, models of communication, scalability issues. In this paper, we will explore the functionalities and the expressiveness of a general-purpose process algebraic framework for the specification and model checking based analysis of collective and cooperative systems. The proposed syntactic and semantic schemes are general enough to be adapted with small modifications to heterogeneous application domains, like, e.g., crowdsourcing systems, trustworthy networks, and distributed ledger technologies.
Bernd Finkbeiner, Jana Hofmann, Florian Kohn, Noemi Passing
Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic construction of smart contract state machines. Towards this end, we extend temporal stream logic (TSL) with universally quantified parameters over infinite domains. Parameterized TSL is a convenient logic to specify the temporal control flow, i.e., the correct order of transactions, as well as the data flow of the contract's fields. We develop a two-step approach that 1) synthesizes a finite representation of the - in general - infinite-state system and 2) splits the system into a compact hierarchical architecture that enables the implementation of the state machine in Solidity. We implement the approach in our prototype tool SCSynt, which - within seconds - automatically constructs Solidity code that realizes the specified control flow.
Sebastian Müller, Andreas Penzkofer, Nikita Polyanskii, Jonas Theis · 6 authors
The Unspent Transaction Output (UTXO) model is commonly used in the field of Distributed Ledger Technology (DLT) to transfer value between participants. One of its advantages is that it allows parallel processing of transactions, as independent transactions can be added in any order. This property of order invariance and parallelisability has potential benefits in terms of scalability. However, since the UTXO Ledger is an append-only data structure, this advantage is compromised through the presence of conflicting transactions. We propose an extended UTXO Ledger model that optimistically updates the ledger and keeps track of the dependencies of the possible conflicts. In the presence of a conflict resolution mechanism, we propose a method to reduce the extended ledger back to a consistent UTXO Ledger.
Purpose The complexity of business environments often causes organizations to produce several inconsistent views of the same business process (BP), leading to fragmentation. BP view integration attempts to produce an integrated view from different views of the same model, facilitating the management of BP models. Design/methodology/approach To study the trends of BP view integration, the authors conduct an extensive and systematic literature review to summarize findings since the 1970s. With a starting corpus of 918 documents, this survey draws up a systematic inventory of solutions used in academia and industry. By narrowing it down to 71 articles, the authors discuss in-depth 17 BP integration techniques papers, classifying each solution according to 9 criteria. Findings The authors' study shows that most view-integration methods (11) utilize annotation-based matching, based on formal merging rules. While most solutions are formalized, only approximately half are validated with a real-world use case scenario. View integration can be applied to areas other than database schema integration and BP view integration. Practical implications By summarizing existing knowledge up to June 2021, the authors explore possible future research directions. The authors highlight the application of view integration to the blockchain research area, where stakeholders can have different views on the same blockchain. The authors expect that this study contributes to interdisciplinary research across view integration, namely to the context of blockchain. Originality/value This survey serves to pave the way for future trends, where the authors highlight the application of view integration to blockchain research.
We discuss the contribution of the Petri net formalism to the BOSE for Smart Contract design and development. We address this discussion based on the analysis of recently published literature works we obtained by querying Scopus and Google Scholar. Different types of Petri nets, including coloured Petri nets and workflow nets, and different types of tools emerge from our analysis. Our discussion includes the classification into three categories of application of the Petri net formalism in the design and development of Smart Contracts, namely modeling, generation, and verification.
Flavio Corradini, Alessandro Marcelletti, Andrea Morichetta, Andrea Polini · 6 authors
A key challenge in engineering distributed systems consists in the integration into their development of a decentralised infrastructure allowing the system participants to trust each other. In this article, we face such a challenge by proposing a model-driven methodology and a related framework to support the engineering of trustable and auditable systems. The approach is based on choreography diagrams specified in the Business Process Model and Notation standard, describing the interactions that should occur among the distributed components of systems. We support the whole lifecycle of choreographies, from their modelling to their distributed execution and auditing. The framework, based on blockchain technology, is named ChorChain. More specifically, ChorChain takes as input a BPMN choreography model and automatically translates it into a Solidity smart contract. The smart contract permits us to enforce the interactions among the cooperating components as prescribed by the choreography model. By leveraging on the auditability of blockchain, ChorChain also supports the activity of auditors continuously. In such a way, ChorChain enables auditors to get some degree of assurance on what happens simultaneously with, or shortly after, information disclosure. We assess the feasibility and effectiveness of the proposed methodology and framework through experiments conducted on the Rinkeby Ethereum Testnet.
The Line-less Mobile Assembly System paradigm (short LMAS) provides necessitated flexibility, especially for large-scale products as customer demands for individualized products persist and product life-cycles remain short. To make LMAS advantages operationally usable in an industrial context, it requires a suitable control system to connect multi-purpose assembly resources and to autonomously configure transient assembly stations. Therefore this paper reviews the relevant literature to identify the necessary components of such architectures. Depending on the control system’s intention and use cases, the properties of the organizational paradigm, an adequate ontology and basic design patterns regarding the distribution and order-relationships of the system entities are to be defined conceptually. For the implementation, a role model, an interaction model, and a data model are required. Due to the utilization of mobile multipurpose resources and the possibility of factory shopfloor reconfiguration by transient stations, existing approaches do not meet LMAS inherent properties. Consequently, we present a suitable decentralized multi-agent control system approach.
Business process modeling and verification have become an essential way to control and assure organizational evolution. We overview the opportunities for the application of blockchain in Business Process Management and Modeling in Finance and we focus on in-depth analysis of claim process in insurance as a use case. We investigate the utilization of blockchain technology for model checking of Workflow, Business Processes to ensure consistency, integrity, and security in a dynamically changing business environment. We create a UML profile for the blockchain, then we combine it with a UML activity diagram followed by a verification using Petri nets to guarantee a distributed computing system and scalable with mutable data. Our paper creates a unified picture of the approaches towards business processes modeling used in the financial industry organized around the set of premises intending to develop a future research agenda for blockchain business process modeling, specifically for the financial industry domain.
Jan 1, 2022·Proceedings of the ... Annual Hawaii International Conference on System Sciences/Proceedings of the Annual Hawaii International Conference on System Sciences
Jan 1, 2022·Proceedings of the ... Annual Hawaii International Conference on System Sciences/Proceedings of the Annual Hawaii International Conference on System Sciences
Considerable progress was forcasted for collaborative business processes with the rise of blockchain programmable platforms. One of the saliant promises was auditable traces of business process execution, but practically that has posed challenges specially with regard to blockchain logs’ structure who turned out to be inadequate for process mining techniques. Approaches to answer this issue have started to emerge in the literature, some focusing on the creation process of event logs and others dealing with their retrieval from the blockchain. This work outlines the generic steps required to solve these challenges and analyzes findings in these approaches with a consideration for efficiency and future research directions.
Jan 1, 2022·Business Process Management: Blockchain, Robotic Process Automation, and Central and Eastern Europe Forum. BPM 2022. Lecture Notes in Business Information Processing, vol 459. Springer, Cham
Blockchain has been proposed to facilitate the enactment of interorganisational business processes. For such processes, blockchain can guarantee the enforcement of rules and the integrity of execution traces - without the need for a centralised trusted party. However, the enactment of interorganisational processes pose manifold challenges. In this work, we ask what answers the research field offers in response to those challenges. To do so, we conduct a systematic literature review (SLR). As our guiding question, we investigate the guarantees and capabilities of blockchain-based enactment approaches. Based on resulting empirical evidence, we develop a taxonomy for blockchain-based enactment. We find that a wide range of approaches support traceability and correctness; however, research focusing on flexibility and scalability remains nascent. For all challenges, we point towards future research opportunities.