This paper investigates the use of Contract Specification Languages (CSLs), smart contracts, and their associated software methods and tools for formally specifying, verifying, and monitoring contracts, as a means to improve compliance with data protection laws, by harnessing the back end of data supply chains. The privacy literature has focused predominantly on B2C relationships (front end data processing) to assess corporate compliance with data protection laws and has explored the use of technologies primarily as a means to empower data subjects vis-à-vis data processors. This article shifts the perspective. First, it shows that the effective implementation of data subjects’ rights hinges upon the capacity of data processors to monitor compliance in back-end processing, i.e., the data supply chain. Second, it spells out the way CSLs and smart contracts can contribute to bridge the compliance gap in the data supply chain, which currently hinders data controllers from effectively monitoring the flow and use of data documents and practices across the networks of subcontractors. Indeed, while data is processed in an iterative and dynamic manner through a wide variety of means by actors within and across companies in the supply chain (e.g., controller, processors, and sub-processors), the legal instruments used to ensure compliance are dispersed, static, convoluted and legalistic, ultimately lacking the capability to operationalize data protection across different management levels (legal, technical, business, etc.). This paper proposes methods for specifying and controlling obligations related to data processing and distributions by using CSLs and smart contracts, and the contribution these methods can make for monitoring compliance in the data supply chain. It briefly introduces the Symboleo CSL for the formal specification of contracts. It then offers a concrete case study testing the properties of the Symboleo in a dataset composed of contractual documents used in the data supply chain of a network of IT companies. The paper concludes with a discussion of the challenges laying ahead to narrow the compliance gap and highlights how the proposed methods can evolve to become effective compliance tools in data protection.

Legal contracts specify requirements for business transactions. Symboleo was recently proposed as a formal specification language for legal contracts. It allows the specification of the contractual requirements by specifying the obligations and powers of the parties, as well as specifying the events that can occur in a contract’s lifecycle. With appropriate tool support, Symboleo can allow monitoring the contract lifecycle. However, because of mistakes in contract interpretation or formal specification, specified contracts may violate properties expected by contracting parties. This paper presents SymboleoPC, a tool for analyzing Symboleo contracts using the nuXmv model checker, where properties can be expressed in both Linear Temporal Logic and Computation Tree Logic. The presentation highlights the architecture, implementation, and testing of the tool, as well as a scalability evaluation, based on performance data. The performance of the tool was evaluated with respect to varying numbers of obligations and powers, with varying numbers of inter-dependencies among them, with parameters derived from the analysis of real contracts. These results suggest that SymboleoPC can be usefully applied to the analysis of formal specifications of contracts with real-life sizes and structures.

Smart contracts (SCs) are software systems that monitor and partially control the execution of legal contracts to ensure compliance with the contracts’ terms and conditions, which essentially are sets of obligations and powers, triggered by events. Such systems often exploit Internet-of-Things technologies to support their monitoring functions and blockchain technology to ensure the integrity of their data. Enterprise-level blockchain platforms (such as Hyperledger Fabric) and public ones (such as Ethereum) are popular choices for SC development. However, usually, legal experts are not able to directly encode contract requirements into SCs. Symboleo is a formal specification language for legal contracts that was introduced to address this issue. Symboleo uses an ontology that defines legal concepts such as parties, obligations, powers, and assets, with semantics expressed with state machines. This paper proposes a tool that automatically translates Symboleo specifications into smart contract code for Hyperledger Fabric. Towards this end, we have extended the current Symboleo IDE, implemented the ontology and semantics by using the modelling language Umple, and created a reusable library. The resulting Symboleo2SC tool generates Hyperledger Fabric code exploiting this library. This code is a complete translation and does not require further development. Symboleo2SC was evaluated with five sample contracts. These were converted to SCs for contract monitoring and control purposes. Symboleo2SC helps simplify the SC development process, saves development effort, and helps reduce risks of coding errors.

Industrial control systems (ICSs), such as Supervisory Control and Data Acquisition (SCADA) systems, are increasingly popular for manufacturing applications, leading to significant improvements in efficiency and productivity. However, the vulnerability of these systems to ransomware attacks has become a major concern. This vulnerability is mainly due to the centralized nature of ICSs, which prioritize efficiency over security. To address this issue, this paper proposes a decentralized Blockchain-Based ICS (BBICS) architecture. Such architecture uses a peer-to-peer network of nodes to replicate critical data and distribute transactions using a consensus mechanism, which synchronizes nodes and resolves single points of failure. Additionally, BBICS encrypts critical data in a tamper-resistant manner to prevent attackers from decrypting or manipulating data. Moreover, zero-trust authorization and authentication further enhance security by preventing the broadcasting of ransomware attacks in internal networks of devices. The evaluation of the proposed system with respect to performance and reliability under normal and ransomware attack situations suggest BBICS’ feasibility and practicality.

Legal contracts specify requirements for business transactions. As any other requirements specification, contracts may contain errors and violate properties expected by contracting parties. Symboleo was recently proposed as a formal specification language for legal contracts. This paper presents SymboleoPC, a tool for analyzing Symboleo contracts using model checking. It highlights the architecture, implementation and testing of the tool, as well as a scalability evaluation with respect to the size of contracts and properties to be checked through a series of experiments. The results suggest that SymboleoPC can be usefully applied to the analysis of formal specifications of contracts with real-life sizes and structures.

Smart contracts (SCs) are software systems that monitor and control the execution of legal contracts to ensure compliance with the contracts' terms and conditions. They often exploit Internet-of-Things technologies to support their monitoring functions, and blockchain technology to ensure the integrity of their data. Ethereum and business blockchain platforms, such as Hyperledger Fabric, are popular choices for SC development. However, there is a gap in the knowledge of SCs between developers and legal experts. Symboleo is a formal specification language for legal contracts that was introduced to address this issue. Symboleo specifications directly encode legal concepts such as parties, obligations, and powers. In this paper, we propose a tool-supported method for translating Symboleo specifications into smart contracts. We have extended the current Symboleo IDE, implemented the ontology and semantics of Symboleo into a reusable library, and developed the Symboleo2SC tool to generate Hyperledger Fabric code exploiting this library. Symboleo2SC was evaluated with three sample contracts. The results shows that legal contract specifications in Symboleo can be fully converted to SCs for monitoring purposes. Moreover, Symboleo2SC helps simplify the SC development process, saves development effort, and helps reduce risks of coding errors.

Legal contracts specify the terms and conditions—in essence, requirements—that apply to business transactions. This paper proposes a formal specification language for legal contracts, called Symboleo, where contracts consist of collections of obligations and powers that define a legal contract’s compliant executions. Symboleo offers execution time operations such as subcontracting, assignment, and substitution. Its formal semantics is defined in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations, and powers. We have implemented two tools to support the analysis of contract specifications. One is a conformance validation tool that enables checking that a specification is consistent with the expectations of contracting parties. The other tool enables model-checking of desired contract properties, expressed in temporal logic. We envision Symboleo with its associated tools as enablers for the formal verification of contracts to detect requirements-level issues. Our proposal includes an evaluation through the specification of two real life-inspired contracts.

Smart contracts (SCs) are software systems that monitor and control the execution of legal contracts to ensure compliance with the contracts' terms and conditions. They often exploit Internet-of-Things technologies to support their monitoring functions, and blockchain technology to ensure the integrity of their data. Ethereum and business blockchain platforms, such as Hyperledger Fabric, are popular choices for SC development. However, there is a gap in the knowledge of SCs between developers and legal experts. Symboleo is a formal specification language for legal contracts that was introduced to address this issue. Symboleo specifications directly encode legal concepts such as parties, obligations, and powers. In this paper, we propose a tool-supported method for translating Symboleo specifications into smart contracts. We have extended the current Symboleo IDE, implemented the ontology and semantics of Symboleo into a reusable library, and developed the Symboleo2SC tool to generate Hyperledger Fabric code exploiting this library. Symboleo2SC was evaluated with three sample contracts. The results shows that legal contract specifications in Symboleo can be fully converted to SCs for monitoring purposes. Moreover, Symboleo2SC helps simplify the SC development process, saves development effort, and helps reduce risks of coding errors.

Social dependance relationships were used in the i* requirements modelling language to represent dependencies among social actors. We study the evolution of the notion of social dependency into that of commitment in the Azzurra specification language for business processes, and then into the notions of obligation and power in the Symboleo specification language for legal contracts. Our account focuses on the difference in the semantics of these relationships, the language used to talk about them, and how appropriate they are for capturing requirements for services.

Smart grids are IoT-enabled grids at which communication devices can be used to interconnect, monitor and manage distributed energy resources (DERs). The emerging efficient and clean energy DERs such as Lithium-ion batteries and Photovoltaic have been widely used in IoT-enabled smart grids that makes their secure operation challenging. In this paper, a blockchain-based IoT platform, namely BIoT, is proposed to maintain security of energy supply network including DERs against IoT platform's security issues, e.g., single point of failure, malicious code and data leak. BIoT verifies resource management requests in a consensus process, provides certificate-based authentication as well as attribute-based access control, and ensures data integrity. BIoT's performance has been evaluated on Ontario Energy Board (OEB) Cybersecurity framework and a performance benchmark.

Through transactive energy (TE) platforms, prosumers can enter into a contractual agreement with an Independent Electricity System Operator (IESO) to buy and sell energy. Accordingly, the TE contract holders are liable for contractual violations. Manual compliance checking of such transactions is infeasible due to large number of market rules as well as the plethora of executing TE contracts. Moreover, the TE system big data (e.g., offers, bids, and transaction activities) need to be maintained on a transparent, reliable, and secure plat-form. This paper presents a compliance checking method for transactive energy markets based on the IESO (in Ontario, Canada) market rules by using smart contracts that assure the integrity, reliability, and transparency of energy transactions’ data with a permissioned blockchain. The performance of the blockchain network is evaluated through transaction latency and resource utilization. In addition, an acceptance test is successfully conducted to validate the correctness of the platform in terms of trading workflow, runtime status of the TE contracts, and the quality of market clearing results.

A contract is a legally binding agreement that expresses high-level requirements of parties in terms of obligations, powers and constraints. Parties’ actions influence the status of a contract and shall comply with its clauses. Manual contract monitoring is very laborious in real markets, such as transactive energy, where plenty of complex contracts are running concurrently. Furthermore, liability, right and performance transition through run-time operations such as subcontracting, assignment and substitution complicate contract interpretation. Automation is needed to ensure that contracts respect desirable properties and to support monitoring of compliance and handling of violations. In this thesis research, I propose an innovative ontology that defines fundamental contractual notions (such as the ones mentioned above) and their relationships, on which is built a specification language, called Symboleo, that provides syntax and axiomatic semantics of contracts via first-order logic. Symboleo enables the development of advanced automation tools such as a compliance checker that monitors contracts at runtime, and a model checking verification method that analyzes liveness and safety properties of contracts. This paper reports on the problem domain, research method, current status, expected contributions, and main foreseen challenges.

Legal contracts specify obligations and powers among legal subjects, involve assets, and are subject to quality constraints. Smart contracts are software systems that monitor the execution of contracts to ensure compliance. As a starting point for developing software engineering concepts, tools, and techniques for smart contracts, we have proposed Symboleo, a formal specification language for contracts. The complexity of real-life contracts (e.g., in the construction and transportation industries) requires specification languages to support execution-time operations for contracts, such as subcontracting, assignment, delegation, and substitution. This paper formalizes such concepts by proposing for them a syntax and axiomatic semantics within Symboleo. This formalization makes use of primitive operations that support the transfer or sharing of right, responsibility, and performance among contracting and subcontracting parties. A prototype compliance checking tool for Symboleo has also been created to support monitoring compliance for contracts that include subcontracting aspects. A realistic freight contract specified in Symboleo is provided as an illustrative example for our proposal, and is used for a preliminary evaluation with positive results.

Legal contracts specify the terms and conditions (in essence, requirements) that apply to business transactions. Smart contracts are software systems that monitor and control the execution of contracts to ensure compliance. This paper proposes a formal specification language for contracts, called Symboleo, where contracts consist of collections of obligations and powers that define the legal contract's compliant executions. The formal semantics of Symboleo is based on an extension of an ontology for Law and is described in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations and powers. Our proposal includes a preliminary evaluation through the specification of a real life-inspired Sale-of-Goods contract, with a prototype execution engine. We envision this language to enable formally verifying contracts to detect requirements-level issues and to generate executable smart contracts (e.g., on blockchain technology).

Nowadays, knowledge is the key to success in all software engineering processes. This valuable knowledge, obtained through analysis, design, development, and maintenance processes of the system, should be saved and reused in designing and developing current and similar systems. Using pre-existing knowledge is a practical approach which reduces design complexity, improves software architecture design and manages software quality. In this paper, we describe an approach to create architecture design knowledge using a hierarchical structure of architectural styles based on quality attributes. Knowledge is most importance asset of our approach that reuses similar domains, correlates architectures and reduces complexity by using and composing rules. Finally, we executed our approach on a standard case study.

We propose a self-adaptive process (SAP) that maintains the software architecture quality using the MAPE-K standard model. The proposed process can be plugged into various software development processes and service-oriented methodologies due to its explicitly defined inputs and outputs. To this aim, the proposed SAP is integrated with the service-oriented modeling and application (SOMA) methodology in a two-layered structure to create a novel methodology, named self-adaptive service-oriented architecture methodology (SASOAM), which provides a semi-automatic self-aware method by the composition of architectural tactics. Moreover, the maintenance activity of SOMA is improved using architectural and adaptive patterns, which results in controlling the software architecture quality. The improvement in the maintainability of SOMA is demonstrated by an analytic hierarchy process (AHP) based evaluation method. Furthermore, the proposed method is applied to a case study to represent the feasibility and practicality of SASOAM.

nowadays, several non-automatic or semi-automatic software architecture evaluation methods have been proposed to evaluate their quality attributes as availability. In spite of their applicability, they are not effective in self-adaptive software architectures due to their off-line properties; e.g., scenario-based methods. Since the architectural tactics provide a bridge between architectural designs and quality attributes, they have sufficient potential to resolve this problem. In this paper, we assume that the software architecture is completely composed of some architectural patterns. Then we propose an automated evaluation method which composes the architectural tactics and the patterns to measure the availability of software architectures. In this method, the composition of a few availability tactics and patterns are simulated with appropriate probability distribution functions. To predict the availability of patterns, a data mining approach is applied to these simulated models to generate training models for each combination of tactics and patterns. Furthermore, a utility function is defined to compute the availability of systems by these models in O(n) where n is the number of patterns of systems. This method improves the data gathering and analysis activities of the SASSY (Self-Architecting Software SYstems) framework. To validate our method, we have applied it to the Rapidminer case study. KeywordsAvailability, Self-Adaptive Architecture, Architectural Tactic, Architectural Pattern, Data Mining.