In the evolving energy landscape where prosumers play an increasingly important role, establishing a secure data exchange architecture is essential for building a resilient and efficient energy infrastructure. Current privacy-preserving systems suffer from inadequate adversarial models, dependence on centralized components, and inability to adapt to evolving threats. This paper introduces the Privacy-Sensitive Distributed Optimization (PSDO) framework, a decentralized management scheme designed to prioritize privacy safeguards in prosumer-driven systems. To achieve this goal, the PSDO framework combines decentralized optimization techniques with differential privacy. This integration serves a dual purpose: preserving prosumers' control over their energy management and ensuring privacy of their sensitive information. By leveraging decentralized optimization, the PSDO framework enables prosumers to maximize the benefits derived from decentralized systems, promoting improved autonomy in energy management. Simultaneously, prosumers' sensitive data is protected through the implementation of differential privacy measures. Through implementation on the IEEE 33-bus radial distribution system, the PSDO algorithm demonstrated its capability to converge to the optimal solution while rigorously upholding differential privacy. PSDO advances beyond the chosen baseline (DP-ADMM) by delivering superior privacy protection while incurring minimal utility loss. Moreover, the framework successfully accommodates diverse privacy preferences while maintaining system-wide efficiency, establishing its effectiveness for heterogeneous prosumers.

The eXtensible Access Control Markup Language (XACML) is a popular OASIS standard for the specification of fine-grained access control policies. However, the standard does not provide a proper solution for the verification of XACML access control policies before their deployment. The first step for the formal verification of XACML policies is to formally specify such policies. Hence, this paper presents XACML2mCRL2, a tool for the automatic translation of XACML access control policies into mCRL2. The mCRL2 specifications generated by our tool can be used for formal verification of important properties of access control policies such as completeness of inconsistency, using the well-known mCRL2 toolset.

The adoption of information technology in foremost sectors of human activity such as banking, healthcare, education, governance etc., increases the amount of data collected and processed to enable these services. With the convenience the technology offers, it also brings increased challenges pertaining to the privacy. In response to these emerging privacy concerns, the European Union has approved the General Data Protection Regulation (GDPR) to strengthen data protection across the European Union. This regulation requires individuals and organizations that process personal data of EU citizens or provide services in EU, to comply with the privacy requirements in the GDPR. However, the privacy policies stating how personal information will be handled to meet regulations as well as organizational objectives, are given in natural language statements. To demonstrate a program's compliance with privacy policies, a link should be established between policy statements and the program code, with the support of a formalized analysis. Based on this vision, we formalize a notion of privacy policies and a notion of compliance for the setting of object-oriented distributed systems. For this we provide explicit constructs to specify constituents of privacy policies (i.e., principal, purpose, access right) on personal data. We present a policy specification language and a formalization of privacy compliance, as well as a high-level modeling language for distributed systems extended with support for policies. We define a type and effect system for static checking of compliance of privacy policies and show soundness of this analysis based on an operational semantics. Finally, we prove a progress property.

We propose a flexible framework for modeling of distributed systems, supporting evolution by means of unrestricted modifications in such systems, and with support of verification and re-verification. We focus on the setting of concurrent and object-oriented programs, and consider a core high-level modeling language supporting active, concurrent objects. We show that our framework can deal with verification of software changes that are not possible to verify in comparable frameworks. We demonstrate the approach by variations over a simple example.

Internet of Things (IoT) offers a variety of technologies for connecting different kinds of heterogeneous devices. Security and privacy are becoming the main issue for IoT systems and their developers. Nevertheless, most works on IoT security and privacy requirements look at these requirements from a high-level view. Hence, the essential aspects of security and privacy functionalities will be disregarded, causing wrong design decisions. To combat this problem, this paper summarizes the most current documents related to security and privacy functionalities in the setting of IoT and provides a new taxonomy framework that organizes all aspects of security and privacy baselines, guidelines, and recommendations. To give an understanding of how the framework can help to improve security and privacy of IoT products, we combine it with a security classification method and demonstrate the usefulness by a case study of health products. Our framework can serve as a cornerstone towards the development of appropriate security solutions.

We introduce Dynamic Structural Operational Semantics (DSOS or Dynamic SOS) as a framework for describing semantics of programming languages that include dynamic software upgrades, i.e., for upgrading software code during run-time. DSOS is built on top of the Modular SOS of P. Mosses, with an underlying category theory formalization. The idea of Dynamic SOS is to bring out the essential differences between dynamic upgrade constructs and program execution constructs. The important feature of Modular SOS (MSOS) that we exploit in DSOS is the sharp separation of the program execution code from the additional (data) structures needed at run-time. In DSOS we aim to achieve the same modularity and decoupling for dynamic software upgrades. This is partly motivated by the long term goal of having machine-checkable proofs for general results like type safety. We exemplify Dynamic SOS on two languages supporting dynamic software upgrades, namely the C-like Proteus, which supports updating of variables, functions, records, or types at specific program points, and Creol, which supports dynamic class upgrades in the setting of concurrent objects. Existing type analyses for software upgrades can be done on top of DSOS too, as we illustrate for Proteus. As a side contribution we define a general encapsulating construction on Modular SOS useful in situations where a form of encapsulation of the execution is needed. We use encapsulation to give modular semantics to the concurrent object-oriented programming language Creol with active objects and asynchronous method invocations.

Today the Internet offers a massive amount of reviews and user experiences about a variety of products from different manufacturers, ranging from smartphones, automobiles, and home appliances to Internet services such as hotel booking and airplane booking. For a careful customer it is time-consuming to make good purchasing decisions due to a variety of similar products, lots of reviews for each product, and distributed reviews on the Internet. To alleviate this situation, this paper proposes EasyChoose, which is a distributed scheme based on Hadoop YARN to continuously collect product reviews from the Internet, extract representative product features based on previous customers' reviews, and highlight the main point of the reviews. In this paper, we use online hotel booking as an example to demonstrate the effectiveness of EasyChoose. The results show that EasyChoose is able to automatically extract representative product features and highlight reviews without losing the original meanings. Furthermore, EasyChoose is able to continuously provide such service to keep up with changes in recent customers' reviews.

Abstract Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. The future mechanism extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed environment. However, futures add a level of complexity to program analysis, as the program semantics becomes more involved. This paper presents a model for asynchronously communicating objects, where return values from method calls are handled by futures. The model facilitates invariant specifications over the locally visible communication history of each object. Compositional reasoning is supported and proved sound, as each object may be specified and verified independently of its environment. A kernel object-oriented language with futures inspired by the ABS modeling language is considered. A compositional proof system for this language is presented, formulated within dynamic logic.

We investigate the usage of a history-based specification approach for concurrent and distributed systems. In particular, we compare two approaches on checking that those systems behave according to their specification. Concretely, we apply runtime assertion checking and static deductive verification on two small case studies to detect specification violations, respectively to ensure that the system follows its specifications. We evaluate and compare both approaches with respect to their scope and ease of application. We give recommendations on which approach is suitable for which purpose as well as the implied costs and benefits of each approach.

Delta-oriented programming is a modular, yet flexible technique to implement software product lines. To efficiently verify the specifications of all possible product variants of a product line, it is usually infeasible to generate all product variants and to verify them individually. To counter this problem, we propose a transformational proof system in which the specifications in a delta module describe changes to previous specifications. Our approach allows each delta module to be verified in isolation, based on symbolic assumptions for calls to methods which may be in other delta modules. When product variants are generated from delta modules, these assumptions are instantiated by the actual guarantees of the methods in the considered product variant and used to derive the specifications of this product variant.

Wireless sensor networks consist of resource constrained nodes, especially with respect to power resources. In many cases, the replacement of a dead node is difficult and costly, e.g. an implanted node in the human body. Our main goal in this paper is reducing the total power consumption of the network. For this purpose, we consider the cooperation of nodes in data transmission in terms of a group, since the major consumer of power is the data transmission process. A mobile node may move to a new location, in which it is desirable for the node to join a group. In this paper, we propose an algorithm for nodes to choose the best group in their signal range, using coalitional game theory to determine what is beneficial in terms of power consumption. The protocol is formalized in rewriting logic, implemented in the Maude tool, and validated by means of Maude's model exploration facilities. Simulation-based tools are in general not able to prove the protocol. However, by using Maude, we prove the correctness of our proposed protocol, by searching for failures of the protocol, through all possible behaviors of sensors. These searches prove that grouping nodes is done correctly in all reachable states from a set of initial states of the model. In addition, we simulate our model in order to quantitatively analyze the efficiency of the proposed protocol. The results show significant improvements in power efficiency.

Convenience in specification and possibility for formal analysis are, to some extent, exclusive aspects of system specification. This paper describes an approach that emphasizes both aspects, by combining UML with a language for observable behavior of interfaces, OUN. These are complementary in the sense that one is graphical and semi-formal while the other is textual and formal. The approach is demonstrated by a case study.

Abstract Partial functions play an important role in computer science. In order to reason about partial functions one may extend classical logic to a logic supporting partial functions, a so-called partial logic. Usually such an extension necessitates side-conditions on classical proof rules in order to ensure consistency, and introduces non-classical proof rules in order to maintain completeness. These complications depend on the choice of consequence relation and non-monotonic operators. In computer science applications such complications are undesirable, because they affect (semi-) mechanical reasoning methods, and make manual reasoning difficult for computer scientists who are not logicians. By carefully choosing the consequence relation and non-monotonic operators, a simple calculus for partial functions arises. The resulting logic is “healthy” in the sense that “meaningless” formulas (such as top(emptystack) > 1) cannot be concluded, except from contradictory or false assumptions, and a meaningless assumption provides no information. This requires all axioms to be healthy; and as a consequence the “excluded middle” ( a V ¬a) must be weakened (to meaningful a's ). All the well-known classical rules preserve healthiness and are therefore sound in the logic, provided substitutions are restricted to meaningful terms. This means that program reasoning methods based on classical logic usually can be adapted to the presented partial logic.

Abstract The aim of this paper is to develop simple and practically useful formalisms for reasoning about processes with shared variables. Our approach is based on the axiomatic system described by Neelam Soundararajan. In contrast to that work, our formalism is first derived from a model; this guarantees soundness and completeness of the formal proof system, with respect to the model. As an additional advantage the rules become simpler than those of Soundararajan; in particular, the local assertions may freely refer to shared variables; and we remove the explicit use of the compatibility predicate. Next we augment the formalism by allowing global invariants, which may refer to shared variables (including shared histories), but with a different semantics than in the local assertions. The augmented system makes reasoning simpler in the sense that reasoning about the past is replaced by reasoning about the present. Finally we suggest a sufficiently complete set of mythical (auxiliary) variables free from embedded program structure. We demonstrate our formalism on some examples.

Abstract Linguistic and semantic consequences of combining the ideas of order sorted algebras (as in OBJ) and generator induction (as in Larch) are investigated. It is found that one can gain the advantages of both, in addition to increased flexibility in defining signatures and generator bases. Our treatment also gives rise to typing control stronger in a certain sense than that of OBJ, as well as the detection of inherently inconsistent signatures.