@article{4792, author = {{Senge, Robin and Hüllermeier, Eyke}}, issn = {{1063-6706}}, journal = {{IEEE Transactions on Fuzzy Systems}}, number = {{6}}, pages = {{2024--2033}}, publisher = {{Institute of Electrical and Electronics Engineers (IEEE)}}, title = {{{Fast Fuzzy Pattern Tree Learning for Classification}}}, doi = {{10.1109/tfuzz.2015.2396078}}, volume = {{23}}, year = {{2015}}, } @misc{333, author = {{Osterbrink, Sebastian}}, publisher = {{Universität Paderborn}}, title = {{{Visualisierung von SMT-Solver-Ausgaben}}}, year = {{2014}}, } @inproceedings{336, abstract = {{Today, service compositions often need to be assembled or changed on-the-fly, which leaves only little time for quality assurance. Moreover, quality assurance is complicated by service providers only giving information on their services in terms of domain specific concepts with only limited semantic meaning. In this paper, we propose a method to construct service compositions based on pre-verifiedtemplates. Templates, given as workflow descriptions, are typed over a (domain-independent) template ontology defining concepts and predicates. Templates are proven correct using an abstract semantics, leaving the specific meaning of ontology concepts open, however, only up to given ontology rules. Construction of service compositions amounts to instantiation of templates with domain-specific services.Correctness of an instantiation can then simply be checked by verifying that the domain ontology(a) adheres to the rules of the template ontology, and (b) fulfills the constraints of the employed template.}}, author = {{Walther, Sven and Wehrheim, Heike}}, booktitle = {{Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS)}}, editor = {{Lanese, Ivan and Madelaine, Eric}}, pages = {{31--48}}, title = {{{Verified Service Compositions by Template-Based Construction}}}, doi = {{10.1007/978-3-319-15317-9_3}}, year = {{2014}}, } @inproceedings{344, author = {{Becker, Matthias and Becker, Steffen and Besova, Galina and Walther, Sven and Wehrheim, Heike}}, booktitle = {{Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (Work in Progress Session)}}, title = {{{Towards Systematic Configuration for Architecture Validation}}}, year = {{2014}}, } @inproceedings{353, abstract = {{There are many technologies for the automation of processesthat deal with services; examples are service discovery and composition.Automation of these processes requires that the services are described semantically. However, semantically described services are currently not oronly rarely available, which limits the applicability of discovery and composition approaches. The systematic support for creating new semanticservices usable by automated technologies is an open problem.We tackle this problem with a template based approach: Domain independent templates are instantiated with domain specific services andboolean expressions. The obtained services have semantic descriptionswhose correctness directly follows from the correctness of the template.Besides the theory, we present experimental results for a service repository in which 85% of the services were generated automatically.}}, author = {{Mohr, Felix and Walther, Sven}}, booktitle = {{Proceedings of the 14th International Conference on Software Reuse (ICSR)}}, pages = {{188--203}}, title = {{{Template-based Generation of Semantic Services}}}, doi = {{10.1007/978-3-319-14130-5_14}}, year = {{2014}}, } @misc{359, author = {{Töws, Manuel}}, publisher = {{Universität Paderborn}}, title = {{{Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIB}}}, year = {{2014}}, } @inproceedings{364, abstract = {{Today, software components are traded on markets in form of services. These services can also be service compositions consisting of several services. If a software architect wants to provide such a service composition in the market for trade, she needs to perform several tasks: she needs to model the composition, to discover existing services to be part of that composition, and to analyze the composition's functional correctness as well as its quality, e.g., performance. Up to now, the architect needed to find and use different tools for these tasks. Typically, these tools are not interoperable with each other. We provide the tool SeSAME that supports a software architect in all of these tasks. SeSAME is an integrated Eclipse-based tool-suite providing a comprehensive service specification language to model service compositions and existing services. Furthermore, it includes modules for service matching, functional analysis, and non-functional analysis. SeSAME is the first tool that integrates all these tasks into one tool-suite and, thereby, provides holistic support for trading software services. Thus, it contributes to a software provider's market success.}}, author = {{Arifulina, Svetlana and Becker, Matthias and Platenius, Marie Christin and Walther, Sven}}, booktitle = {{Proceedings of the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014)}}, pages = {{839--842}}, title = {{{SeSAME: Modeling and Analyzing High-Quality Service Compositions}}}, doi = {{10.1145/2642937.2648621}}, year = {{2014}}, } @inproceedings{449, abstract = {{Cloud computing resulted in a continuously growing number of provided software services to be used by consumers. Brokers discover services that fit best to consumers' requirements by matching Qualityof-Service (QoS) properties. In order to negotiate Service-Level Agreements (SLAs), a provider has to determine the provided QoS based on QoS analyses. However, the risk for the provider to violate the SLA is high as the service's actual quality can deviate from the specified QoS due to uncertainties that occur during the provider's quality analysis. In this paper, we discuss current software engineering paradigms like cloud computing and service-oriented computing with respect to the amount of uncertainty they induce into service matching and SLA negotiations. As a result, we explain, why cloud computing reduces such uncertainties.}}, author = {{Becker, Matthias and Platenius, Marie Christin and Becker, Steffen}}, booktitle = {{Proceedings of the 2nd International Workshop on Cloud Service Brokerage (CSB)}}, pages = {{153--159}}, title = {{{Cloud Computing Reduces Uncertainties in Quality-of-Service Matching!}}}, doi = {{10.1007/978-3-319-14886-1_15}}, year = {{2014}}, } @inproceedings{402, abstract = {{Various approaches in service engineering are based on servicemarkets where brokers use service matching in order to performservice discovery. For matching, a broker translates the specifications ofproviders' services and requesters' requirements into her own specificationlanguage, in order to check their compliance using a matcher. Thebroker's success depends on the configuration of her language and itsmatcher because they in uence important properties like the effort forproviders and requesters to create suitable specifications as well as accuracyand runtime of matching. However, neither existing service specification languages, nor existing matching approaches are optimized insuch way. Our approach automatically provides brokers with an optimalconfiguration of a language and its matcher to improve her success ina given market with respect to her strategy. The approach is based onformalized configuration properties and a predefined set of configurationrules.}}, author = {{Arifulina, Svetlana and Platenius, Marie Christin and Gerth, Christian and Becker, Steffen and Engels, Gregor and Schäfer, Wilhelm}}, booktitle = {{Proceedings of the 12th International Conference on Service Oriented Computing (ICSOC 2014)}}, editor = {{Franch, Xavier and Ghose, AdityaK. and Lewis, GraceA. and Bhiri, Sami}}, pages = {{543--550}}, title = {{{Market-optimized Service Specification and Matching}}}, doi = {{10.1007/978-3-662-45391-9_47}}, year = {{2014}}, } @inproceedings{409, abstract = {{Service markets provide software components in the formof services. In order to enable a service discovery that satisfies servicerequesters and providers best, markets need automatic service matching:approaches for comparing whether a provided service satisfies a servicerequest. Current markets, e.g., app markets, are limited to basic keywordbasedsearch although many better suitable matching approaches aredescribed in literature. However, necessary architectural decisions forthe integration of matchers have a huge impact on quality propertieslike performance or security.Architectural decisions wrt. servicematchers have rarely been discussed,yet, and systematic approaches for their integration into service marketsare missing. In this paper, we present a systematic integration approachincluding the definition of requirements and a discussion on architecturaltactics. As a benefit, the decision-making process of integrating servicematchers is supported and the overall market success can be improved.}}, author = {{Platenius, Marie Christin and Becker, Steffen and Schäfer, Wilhelm}}, booktitle = {{Proceedings of the 8th European Conference on Software Architecture (ECSA 2014)}}, editor = {{Avgeriou, Paris and Zdun, Uwe}}, pages = {{210--217}}, title = {{{Integrating Service Matchers into a Service Market Architecture}}}, doi = {{10.1007/978-3-319-09970-5_19}}, year = {{2014}}, } @inproceedings{417, abstract = {{Model transformation is a key concept in modeldrivensoftware engineering. The definition of model transformationsis usually based on meta-models describing the abstractsyntax of languages. While meta-models are thereby able to abstractfrom superfluous details of concrete syntax, they often loosestructural information inherent in languages, like information onmodel elements always occurring together in particular shapes.As a consequence, model transformations cannot naturally re-uselanguage structures, thus leading to unnecessary complexity intheir development as well as analysis.In this paper, we propose a new approach to model transformationdevelopment which allows to simplify and improve thequality of the developed transformations via the exploitation ofthe languages’ structures. The approach is based on context-freegrammars and transformations defined by pairing productions ofsource and target grammars. We show that such transformationsexhibit three important characteristics: they are sound, completeand deterministic.}}, author = {{Besova, Galina and Steenke, Dominik and Wehrheim, Heike}}, booktitle = {{Proceedings 3rd Workshop on Model Driven Approaches in System Development (MDASD)}}, pages = {{1601--1610}}, title = {{{Grammar-based model transformations}}}, doi = {{10.1016/j.cl.2015.05.003}}, year = {{2014}}, } @misc{422, author = {{Sanati, Maryam}}, publisher = {{Universität Paderborn}}, title = {{{Formal Semantics of Probabilistic SMT Solving in Verification of Service Compositions}}}, year = {{2014}}, } @misc{423, author = {{Jojiju, Suman}}, publisher = {{Universität Paderborn}}, title = {{{Finding Optimal Self-Adaption Rules by Design-Space Exploration}}}, year = {{2014}}, } @misc{427, author = {{Bulk, Benjamin}}, publisher = {{Universität Paderborn}}, title = {{{Evaluating the Influence of Different Abstraction Levels of Software Design on Performance prediction}}}, year = {{2014}}, } @misc{430, author = {{Krakau, Andreas}}, publisher = {{Universität Paderborn}}, title = {{{Entwicklung eines Konzepts zur Kodierung eines objektorientierten Typsystems in SMT}}}, year = {{2014}}, } @misc{472, author = {{Engelbrecht, Marco}}, publisher = {{Universität Paderborn}}, title = {{{Vergleichsstudie zur Ausdrucksstärke von SMT-Solvern}}}, year = {{2013}}, } @inproceedings{483, abstract = {{Modern software systems adapt themselves to changing environments, to meet quality-of-service requirements, such as response time limits. The engineering of the system’s self-adaptation logic does not only require new modeling methods, but also new analyzes of transient phases. Model-driven software performance engineering methods already allow design-time analysis of steady states of non-adaptive system models. In order to validate requirements for transient phases, new modeling and analysis methods are needed. In this paper, we present SimuLizar, our initial model-driven approach to model self-adaptive systems and analyze the performance of their transient phases. Our evaluation of a load balancer toy example shows the applicability of our modeling approach. Additionally, a comparison of our performance analysis with a prototypical implementation of our example system shows that the prediction accuracy is sufficient to identify unsatisfactory self-adaptations.}}, author = {{Becker, Matthias and Becker, Steffen and Meyer, Joachim}}, booktitle = {{Proceedings of the Software Engineering Conference (SE)}}, pages = {{71--84}}, title = {{{SimuLizar: Design-Time modeling and Performance Analysis of Self-Adaptive Systems}}}, year = {{2013}}, } @inproceedings{502, abstract = {{Self-adaptation allows continuously running software systems to operate in changing and uncertain contexts while meeting their requirements in a broad range of contexts, e.g., from low to high load situations. As a consequence, requirementsfor self-adaptive systems are more complex than requirements for static systems as they have to explicitly address properties of the self-adaptation layer.While approaches exist in the literature to capture this new type of requirements formally, their achievement cannot be analyzed in early design phases yet. In this paper, we apply RELAX to formally specify non-functional requirements for self-adaptive systems. We then apply our model-based SimuLizar approach for a semi-automatic analysis to test whether the self-adaptation layer ensures that these non-functional requirements are met. We evaluate our approach on the design of a proof-of-concept load balancer system. As this evaluation demonstrates, we can iteratively improve our system design by improving unsatisfactory self-adaption rules.}}, author = {{Becker, Matthias and Luckey, Markus and Becker, Steffen}}, booktitle = {{Proceedings of the 9th ACM SigSoft International Conference on Quality of Software Architectures (QoSA'13)}}, pages = {{43--52 }}, title = {{{Performance Analysis of Self-Adaptive Systems for Requirements Validation at Design-Time}}}, doi = {{10.1145/2465478.2465489}}, year = {{2013}}, } @inproceedings{517, abstract = {{In the Semantic (Web) Services area, services are considered black boxes with a semantic description of their interfaces as to allow for precise service selection and configuration. The semantic description is usually grounded on domain-specific concepts as modeled in ontologies. This accounts for types used in service signatures, but also predicates occurring in preconditions and effects of services. Ontologies, in particular those enhanced with rules, capture the knowledge of domain experts on properties of and relations between domain concepts. In this paper, we present a verification technique for service compositions which makes use of this domain knowledge. We consider a service composition to be an assembly of services of which we just know signatures, preconditions, and effects. We aim at proving that a composition satisfies a (user-defined) requirement, specified in terms of guaranteed preconditions and required postconditions. As an underlying verification engine we use an SMT solver. To take advantage of the domain knowledge (and often, to enable verification at all), the knowledge is fed into the solver in the form of sorts, uninterpreted functions and in particular assertions as to enhance the solver’s reasoning capabilities. Thereby, we allow for deductions within a domain previously unknown to the solver. We exemplify our technique on a case study from the area of water network optimization software.}}, author = {{Walther, Sven and Wehrheim, Heike}}, booktitle = {{Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS)}}, pages = {{24 -- 32 }}, title = {{{Knowledge-Based Verification of Service Compositions - An SMT approach}}}, doi = {{10.1109/ICECCS.2013.14}}, year = {{2013}}, } @inproceedings{529, abstract = {{Mechatronic systems reconfigure the structure of their software architecture, e.g., to avoid hazardous situations or to optimize operational conditions like minimizing their energy consumption. As software architectures are typically build on components, reconfiguration actions need to respect the component structure. This structure should be hierarchical to enable encapsulated components. While many reconfiguration approaches for embedded real-time systems allow the use of hierarchically embedded components, i.e., horizontal composition, none of them offers a modeling and verification solution to take hierarchical composition, i.e., encapsulation, into account. In this paper, we present an extension to our existing modeling language, MechatronicUML, to enable safe hierarchical reconfigurations. The two main extensions are (a) an adapted variant of the two-phase commit protocol to initiate reconfigurations which maintain component encapsulation and (b) a timed model checking verification approach for instances of our model. We illustrate our approach on a case study in the area of smart railway systems by showing two different use cases of our approach and the verification of their safety properties.}}, author = {{Heinzemann, Christian and Becker, Steffen}}, booktitle = {{Proceedings of the 16th International ACM SigSoft Symposium on Component-Based Software Engineering (CBSE)}}, pages = {{3--12}}, title = {{{Executing Reconfigurations in Hierarchical Component Architectures}}}, doi = {{10.1145/2465449.2465452}}, year = {{2013}}, }