Search

The choice of an adequate notation and subsequent system formalization are the crucial points for the design of cyber-physical systems (CPSs). Here, an appropriate notation allows an explicit specification of the deterministic system behavior for specified initial states and inputs. We base our study on an industrial example (water tank) that comprises nominal as well as safety-critical states, and focus on the notation’s support to validate/verify crucial safety properties. Several industrial notations (e.g. Matlab/Simulink©) to design and simulate such a hybrid system have been tried based on our physical model. In addition, we remodel our example using the well-founded mathematical formalism of hybrid automata. It enables us to formally express and verify important safety properties using the theorem prover KeYmaera.

With adoption of the UML and other graphical languages by software industry,graphical models became a cornerstone in today's software development practice.As other artefacts such as program source code, graphical models evolve overtime and are, thus, put regularily under version control.In order to deeply understand the role an artefact plays within a project, it issometimes helpful to review the history of this artefact. While there arenumerous tools available that make it easy for a user to grasp the evolution oftextual files (or even portions of it), an adequate support for graphical fileshas remained to be an area of niche products.In this paper, we argue that a better support for reviewing the version historyof graphical files can facilitate the work with graphical models. In order tosupport this claim, we implemented a prototypcical tool that can extract anddisplay the version history of any graphical file stored in a GitHub-repository.In addition, users can annotate each version of a file with comments, whatturns our tool into a review tool for software projects. Recently, we started touse the tool is a software engineering course to give students better feedbackon complex UML models they have to develop iteratively.

Until now, privacy protections have focused on guaranteeing individuals a measure of control over information relating to themselves. However, in the digital age, this protection has become less effective since data is constantly collected and stored in ways that make it difficult for the individual to have control over each piece of information. Furthermore, the information communicated by an individual, when processed in conjunction with other data points, may allow potentially harmful inferences to be drawn about other individuals and the groups to which they may belong. The potential of Big Data to harm groups, particularly in fragile contexts or areas of weak statehood, therefore raises a number of questions which this chapter seeks to explore: is there such a thing as group privacy, distinct from individual privacy? Is group privacy a workable concept? If so, should it be a legally enforceable right and how can it be protected? We begin by exploring various concepts of privacy and group; then discuss how to affirm and protect group privacy through a combination of traditional levers of power and better data management, security, and literacy.

A Domain-Specific Language (DSL) allows the succinct modeling of phenomena in a problem domain. Modern DSL-tools make it easy for a language designer to define the syntax of a new DSL, to specify code generators or to build a new DSL on top of existing DSLs. Based on the language specification, the DSL-tool then generates rich editors. Often, these editors support features such as syntax highlighting, code completion or automatic refactoring.

Due to their complexity, the syntax of modern modeling languages is preferably defined in two steps. The abstract syntax identifies all modeling concepts whereas the concrete syntax should clarify how these concepts are rendered by graphical and/or textual elements. While the abstract syntax is often defined in form of a metamodel, there does not exist such standard format yet for concrete syntax definitions. The diversity of definition formats-ranging from EBNF grammars to informal text-is becoming a major obstacle for advances in modeling language engineering, including the automatic generation of editors. In this paper, we propose a uniform format for concrete syntax definitions. Our approach captures both textual and graphical model representations and even allows to assign more than one rendering to the same modeling concept. Consequently, following our approach, a model can have multiple, fully equivalent representations, but-in order to avoid ambiguities when reading a model representation-two different models should always have distinguishable representations. We call a syntax definition correct, if all well-formed models are represented in a non-ambiguous way. As the main contribution of this paper, we present a rigorous analysis technique to check the correctness of concrete syntax definitions.

KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an integrated manner. Formal specification is performed using the Object Constraint Language (OCL), which is part of the UML standard. KeY provides support for the authoring and formal analysis of OCL constraints. The target language of KeY based development is Java Card DL, a proper subset of Java for smart card applications and embedded systems. KeY uses a dynamic logic for Java Card DL to express proof obligations, and provides a state-of-the-art theorem prover for interactive and automated verification. Apart from its integration into UML based software development, a characteristic feature of KeY is that formal specification and verification can be introduced incrementally.

The purpose of the paper is to present our approach for specifying system behavior during analysis, part of the Fondue software development method. The approach is exemplified on a case study, a Drink Vending Machine (DVM). It is based on Operation Schemas and a Protocol Model. The Protocol Model describes the temporal ordering of the system operations by an UML protocol statemachine. An Operation Schema describes the functionality of a system operation by pre- and postconditions; they are written in the Object Constraint Language (OCL), with a few amendments and extensions. Our approach offers a middle ground between the informal descriptions of Use Cases and the solution-oriented models of object interaction in UML. We believe that declarative behavioral specification techniques, like the one proposed in this paper, lead to more confidence in the quality of the software because they allow one to reason about system properties.

The Distributed Algorithms Working Notation (DAWN) was designed for modelling and verifying algorithms in an intuitive way. Nevertheless, DAWN proofs are formal. In this paper, we show that it is possible to check correctness of a DAWN proof fully automatically: For each step in a DAWN proof, we can generate a set of proof obligations which can automatically be checked by help of automated theorem provers. The verification tool ILF provides a uniform interface to many theorem provers—which makes it an ideal partner for DAWN and a basis for building a DAWN-tool.

When writing a Java library, it is very difficult to hide functionality that is intended not to be used by clients. The visibility concept of Java often forces the developer to expose implementation details. Consequently, we find a high number of public classes and methods in many Java libraries. Thus, client programmers must rely on documentation in order to identify the entry points of the library, i.e. the methods originally intended to be used by clients. In this paper, we introduce a new metric, called the Method Weight , that assists in detecting entry points. Applying this metric on some well-known open-source Java libraries considerably supported the process of identifying their entry points. Furthermore, the metric provides a classification criterion to distinguish libraries with focused functionality from plain collections of utility classes.

The functional specification of software systems is often given in form of use cases. The compliance of a system implementation to a use case specification is validated by system tests, which can nowadays be automated. Unfortunately, system tests run slowly and assume that all needed external systems such as databases and authentication servers are accessible and run correctly. For these reasons, software developers rather rely on module tests, which test the functionality of individual modules. Module tests, however, have the disadvantage of being defined independently of the customer's system specification. In this paper, we describe an approach to combine the advantages of system and module tests. The core technique is (i) to record the complete information flow between modules during the execution of system tests and (ii) to generate, based on this data, corresponding module tests afterwards. The resulting module tests are fast, they are independent of external systems, and they reflect test scenarios defined in use cases. Our approach is heavily based on aspect-oriented programming (AOP) and implemented by the open-source framework jautomock.

Refactoring is a powerful technique to improve the quality of software models including implementation code. The software developer applies successively so-called refactoring rules on the current software model and transforms it into a new model. Ideally, the application of a refactoring rule preserves the semantics of the model, on which it is applied. In this paper, we present a simple criterion and a proof technique for the semantic preservation of refactoring rules that are defined for UML class diagrams and OCL constraints. Our approach is based on a novel formalization of the OCL semantics in form of graph transformation rules. We illustrate our approach using the refactoring rule MoveAttribute.

Many popular methodologies are influenced by Design by Contract. They recommend to specify the intended behavior of operations in an early phase of the software development life cycle. In practice, software developers use most often natural language to describe how the state of the system is supposed to change when the operation is executed. Formal contract specification languages are still rarely used because their semantics often mismatch the needs of software developers. Restrictive specification languages usually suffer from the ”frame problem”: It is hard to express which parts of the system state should remain unaffected when the specified operation is executed. Constructive specification languages, instead, suffer from the tendency to make specifications deterministic. This paper investigates how a combination of OCL and graph transformations can overcome the frame problem and can make constructive specifications less deterministic. Our new contract specification language is considerably more expressive than both pure OCL and pure graph transformations