检索结果-内蒙古大学图书馆

A modeling framework for the development of provably secure E-commerce applications

学校读者我要写书评

暂无评论

A modeling framework for the development of provably secure ...

2nd International Conference on software engineering Advances - ICSEA 2007

作者： Moebius, Nina Haneberg, Dominik Reif, Wolfgang Schellhorn, Gerhard Institute of Computer Science University Augsburg Department of Software Engineering and Programming Languages 86135 Augsburg Germany

ISBN: (纸本)0769529372

Developing security-critical applications is very difficult and the past has shown that many applications turned out to be erroneous after years of usage. For this reason it is desirable to have a sound methodology for developing security-critical E-Commerce applications. We present an approach to model these applications with the unified modeling language (UML) [1] extended by a UML profile to tailor our models to security applications. Our intent is to (semi-) automatically generate a formal specification suitable for verification as well as an implementation from the model. Therefore we offer a development method seamlessly integrating semi-formal and formal methods as well as the implementation. This is a significant advantage compared to other approaches not dealing with all aspects from abstract models down to code. Based on this approach we can prove security properties on the abstract protocol level as well as the correctness of the protocol implementation in Java with respect to the formal model using the refinement approach. In this paper we concentrate on the modeling with UML and some details regarding the transformation of this model into the formal specification. We illustrate our approach on an electronic payment system called Mondex [10]. Mondex has become famous for being the target of the first ITSEC evaluation of the highest level E6 which requires formal specification and verification. © 2007 IEEE.

关键词： Unified Modeling Language

A domain-specific language for modeling and analyzing solution spaces for technology roadmapping

学校读者我要写书评

暂无评论

arXiv 2021年

作者： Breckel, Alexander Pietron, Jakob Juhnke, Katharina Sihler, Florian Tichy, Matthias Institute of Software Engineering and Programming Languages Ulm University Ulm Germany

The introduction of major innovations in industry requires a collaboration across the whole value chain. A common way to organize such a collaboration is the use of technology roadmaps, which act as an industry-wide long-term planning tool. Technology roadmaps are used to identify industry needs, estimate the availability of technological solutions, and identify the need for innovation in the future. Roadmaps are inherently both time-dependent and based on uncertain values, i.e., properties and structural components can change over time. Furthermore, roadmaps have to reason about alternative solutions as well as their key performance indicators. Current approaches for model-based engineering do not inherently support these aspects. We present a novel model-based approach treating those aspects as first-class citizens. To address the problem of missing support for time in the context of roadmap modeling, we introduce the concepts of a common global time, time-dependent properties, and time-dependent availability. This includes requirements, properties, and the structure of the model or its components as well. Furthermore, we support the specification and analysis of key performance indicators for alternative solutions. These concepts result in a continuous range of various valid models over time instead of a single valid model at a certain point of time. We present a graphical user interface to enable the user to efficiently create and analyze those models. We further show the semantics of the resulting model by a translation into a set of global constraints as well as how we solve the resulting constraint system. We report on the evaluation of these concepts and the Iris tool with domain experts from different companies in the automotive value chain based on the industrial case of a smart sensing electrical fuse. © 2021, CC BY-NC-ND.

关键词： Problem oriented languages

The Impact of Model Transformation Language Features on Quality Properties of MTLs: A Study Protocol

学校读者我要写书评

暂无评论

arXiv 2022年

作者： Höppner, Stefan Tichy, Matthias Ulm University Institute of Software Engineering and Programming Languages Ulm Germany

Background: Dedicated model transformation languages are claimed to provide many benefits over the use of general purpose languages for developing model transformations. However, the actual advantages and disadvantages associated with the use of model transformation languages are poorly understood empirically. There is little knowledge over what advantages and disadvantages hold in which cases and where they originate from. In a prior interview study, we elicited expert opinions on what advantages result from what factors surrounding model transformation languages as well as a number of moderating factors that moderate the influence. Objective: We aim to quantitatively asses the interview results to confirm or reject the influences and moderation effects posed by different factors and to gain insights into how valuable different factors are to the discussion. Method: We gather data on the factors and quality attributes using an online survey. To analyse the data and examine the hypothesised influences and moderations we use universal structure modelling based on a structural equation model. Universal structure modelling will produce significance values and path coefficients for each hypothesised and modelled interdependence between factors and quality attributes that can be used to confirm or reject correlation and to weigh the strength of influence present. Limitations: Due to the complexity and abstractness of the concepts under investigation, a measurement via reflective or formative indicators is not possible. Instead participants are queried about their assessment of concepts through a single item question. We further assume that positive and negative effects of a feature are more prominent if the feature is used more frequently. © 2022, CC BY.

关键词： Surveys

Efficient Caching for Operation-Based Versioning

学校读者我要写书评

暂无评论

Efficient Caching for Operation-Based Versioning

Conference on Model Driven engineering languages and Systems Companion (MODELS-C)

作者： Jakob Pietron Heiko Raab Matthias Tichy Institute of Software Engineering and Programming Languages Ulm University Ulm Germany

Context: Operation-based versioning introduces the benefit of meaningful edit histories. However, to load a distinct prior version, it must be restored by reapplying all previous operations, which is time-consuming and interrupts the user's workflow. Caching helps to overcome this problem to the cost of increasing memory requirements. Further, there is no caching approach supporting branches, merges, and possibly resolved conflicts. Objective: We developed an adaptive caching strategy capable of the previously mentioned features. The adaptive strategy aims at reducing the memory in use by garbage collecting aged caches by not using the same static distance between two caches across the whole edit history. Instead, the distance increases depending on a version's age and its distance to a branch's head. Method: We conducted a controlled experiment with models of several sizes and compared the time to restore model versions and the memory in use for no caching, static caching, and our developed adaptive caching. Results: Adaptive caching decreases the time to restore a version to 0.0007 % and 8.3 % compared to no caching. While static caching performs slightly better, it uses 70 % more memory than adaptive caching. Conclusion: Our adaptive caching strategy performs well on models with branches and merges and reduces the time to restore below thresholds which would negatively impact the user experience.

关键词：

A Domain-Specific Language and Interactive User Interface for Model-Driven engineering of Technology Roadmaps

学校读者我要写书评

暂无评论

A Domain-Specific Language and Interactive User Interface fo...

Euromicro Conference on software engineering and Advanced Applications (SEAA)

作者： Alexander Breckel Jakob Pietron Katharina Juhnke Matthias Tichy Institute of Software Engineering and Programming Languages Ulm University Ulm Germany

ISBN: (数字)9781728195322

ISBN: (纸本)9781728195339

The introduction of major innovations in industry requires a collaboration across the whole supply chain. A common way to organize such a collaboration is the use of technology roadmaps, which act as an industry-wide long-term planning tool. Technology roadmaps are used to identify industry needs, estimate the availability of technological solutions, and identify the need for innovation in the future. Roadmaps are inherently both time-dependent and based on uncertain values, i.e., properties and structural components can change over time. Current approaches for model-driven engineering do not inherently support these aspects. We present a novel model-driven approach treating those aspects as first-class citizens. To address the problem of missing support for time in the context of roadmap modeling, we introduce the concepts of a common global time, time-dependent properties, and time-dependent availability. This includes requirements, properties, and the structure of the model or its components as well. These concepts result in a continuous range of various valid models over time instead of a single valid model at a certain point of time. We present concepts for an interactive graphical user interface to enable the user to efficiently interact with those models. We illustrate the application of these concepts on an industrial example of a next generation electrical fuse.

关键词： Fuses Unified modeling language Tools Technological innovation Switches Analytical models Automobiles

Checking Consistency of Robot software Architectures in ROS

学校读者我要写书评

暂无评论

Checking Consistency of Robot Software Architectures in ROS

Workshop on Robotics software engineering (RoSE)

作者： Thomas Witte Matthias Tichy Software Engineering and Programming Languages Ulm University

Context: The software architecture of complex robot systems is usually divided into components. The software is then the configuration and combination of those components and their connectors. Objective: In the Robot Operating System (ROS), this architectural configuration, the ROS node graph, is partly defined in code and created at run-time. The static information about the architecture in the configuration is limited and checking the consistency at development time is not possible. The full software has to be manually executed to check the consistency and debug configuration errors. Method: We propose an approach and a corresponding tool to analyze ROS nodes and their launch files to check consistency and issue warnings if potential problems are detected. The approach uses both static analysis of the launch files as well as dynamic analysis of individual ROS nodes to reconstruct the node graph without executing the whole launch configuration. The nodes are executed in a sandbox to prevent side effects and enable the integration of the analysis tool, e.g., into automated testing systems. Results: The evaluation on internal and publicly available ROS projects shows that we are able to reconstruct the complete architecture of the system if the nodes implement a common lifecycle. Conclusion: The approach enables ROS developers to avoid creating incompatible architectures and check consistency already at development time. The approach can be extended to also monitor architectural consistency at run time.

关键词： Robots Tools Computer architecture Peer-to-peer computing software architecture Prototypes Testing

A decidable confluence test for cognitive models in ACT-R

学校读者我要写书评

暂无评论

arXiv 2017年

作者： Gall, Daniel Frühwirth, Thom Institute of Software Engineering and Programming Languages Ulm University Ulm89069 Germany

Computational cognitive modeling investigates human cognition by building detailed computational models for cognitive processes. Adaptive Control of Thought – Rational (ACT-R) is a rule-based cognitive architecture that offers a widely employed framework to build such models. There is a sound and complete embedding of ACT-R in Constraint Handling Rules (CHR). Therefore analysis techniques from CHR can be used to reason about computational properties of ACT-R models. For example, confluence is the property that a program yields the same result for the same input regardless of the rules that are applied. In ACT-R models, there are often cognitive processes that should always yield the same result while others e.g. implement strategies to solve a problem that could yield different results. In this paper, a decidable confluence criterion for ACT-R is presented. It allows to identify ACT-R rules that are not confluent. Thereby, the modeler can check if his model has the desired behavior. The sound and complete translation of ACT-R to CHR from prior work is used to come up with a suitable invariant-based confluence criterion from the CHR literature. Proper invariants for translated ACT-R models are identified and proven to be decidable. The presented method coincides with confluence of the original ACT-R models. Copyright © 2017, The Authors. All rights reserved.

关键词： Computability and decidability

How to Drawjectory? - Trajectory Planning using programming by Demonstration

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Alkewitz, Leonhard Zuccarello, Timo Raschke, Alexander Tichy, Matthias Institute of Software Engineering and Programming Languages Ulm University Ulm89081 Germany

A flight trajectory defines how exactly a quadrocopter moves in the three-dimensional space from one position to another. Automatic flight trajectory planning faces challenges such as high computational effort and a lack of precision. Hence, when low computational effort or precise control is required, programming the flight route trajectory manually might be preferable. However, this requires in-depth knowledge of how to accurately plan flight trajectories in three-dimensional space. We propose planning quadrocopter flight trajectories manually using the programming by Demonstration (PbD) approach – simply drawing the trajectory in the three-dimensional space by hand. This simplifies the planning process and reduces the level of in-depth knowledge required. We implemented the approach in the context of the Quadcopter Lab at ulm university. In order to evaluate our approach, we compare the precision and accuracy of the trajectories drawn by a user using our approach as well as the required time with those manually programmed using a domain specific language. The evaluation shows that the Drawjectory workflow is, on average, 78.7 seconds faster without a significant loss of precision, shown by an average deviation 6.67 cm. © 2024, CC BY.

关键词： Flight paths

Confluence modulo equivalence with invariants in constraint handling rules

学校读者我要写书评

暂无评论

arXiv 2018年

作者： Gall, Daniel Frühwirth, Thom Institute of Software Engineering and Programming Languages Ulm University Ulm89069 Germany

Confluence denotes the property of a state transition system that states can be rewritten in more than one way yielding the same result. Although it is a desirable property, confluence is often too strict in practical applications because it also considers states that can never be reached in practice. Additionally, sometimes states that have the same semantics in the practical context are considered as different states due to different syntactic representations. By introducing suitable invariants and equivalence relations on the states, programs may have the property to be confluent modulo the equivalence relation w.r.t. the invariant which often is desirable in practice. In this paper, a sufficient and necessary criterion for confluence modulo equivalence w.r.t. an invariant for Constraint Handling Rules (CHR) is presented. It is the first approach that covers invariant-based confluence modulo equivalence for the de facto standard semantics of CHR. There is a trade-off between practical applicability and the simplicity of proving a confluence property. Therefore, a better manageable subset of equivalence relations has been identified that allows for the proposed confluence criterion and and simplifies the confluence proofs by using well established CHR analysis methods. Copyright © 2018, The Authors. All rights reserved.

关键词： Semantics