@article{DiehlMayerMayeretal.2015, author = {Diehl, Katharina and Mayer, Manfred and Mayer, Frank and G{\"o}rig, Tatiana and Bock, Christina and Herr, Raphael M. and Schneider, Sven}, title = {Physical Activity Counseling by Primary Care Physicians: Attitudes, Knowledge, Implementation, and Perceived Success}, series = {Journal of physical activity and health}, volume = {12}, journal = {Journal of physical activity and health}, number = {2}, publisher = {Human Kinetics Publ.}, address = {Champaign}, issn = {1543-3080}, doi = {10.1123/jpah.2013-0273}, pages = {216 -- 223}, year = {2015}, abstract = {Background: In physical activity (PA) counseling, primary care physicians (PCPs) play a key role because they are in regular contact with large sections of the population and are important contact people in all health-related issues. However, little is known about their attitudes, knowledge, and perceived success, as well as about factors associated with the implementation of PA counseling. Methods: We collected data from 4074 PCPs including information on physician and practice characteristics, attitudes toward cardiovascular disease (CVD) prevention, and measures used during routine practice to prevent CVD. Here, we followed widely the established 5 A's strategy (Assess, Advise, Agree, Assist, Arrange). Results: The majority (87.2\%) of PCPs rated their own level of competence in PA counseling as 'high,' while 52.3\% rated their own capability to motivate patients to increase PA as 'not good.' Nine of ten PCPs routinely provided at least 1 measure of the modified 5 A's strategy, while 9.5\% routinely used all 5 intervention strategies. Conclusions: The positive attitude toward PA counseling among PCPs should be supported by other stakeholders in the field of prevention and health promotion. An example would be the reimbursement of health counseling services by compulsory health insurance, which would enable PCPs to invest more time in individualized health promotion.}, language = {en} } @article{SchneiderLambersOrejas2018, author = {Schneider, Sven and Lambers, Leen and Orejas, Fernando}, title = {Automated reasoning for attributed graph properties}, series = {International Journal on Software Tools for Technology Transfer}, volume = {20}, journal = {International Journal on Software Tools for Technology Transfer}, number = {6}, publisher = {Springer}, address = {Heidelberg}, issn = {1433-2779}, doi = {10.1007/s10009-018-0496-3}, pages = {705 -- 737}, year = {2018}, abstract = {Graphs are ubiquitous in computer science. Moreover, in various application fields, graphs are equipped with attributes to express additional information such as names of entities or weights of relationships. Due to the pervasiveness of attributed graphs, it is highly important to have the means to express properties on attributed graphs to strengthen modeling capabilities and to enable analysis. Firstly, we introduce a new logic of attributed graph properties, where the graph part and attribution part are neatly separated. The graph part is equivalent to first-order logic on graphs as introduced by Courcelle. It employs graph morphisms to allow the specification of complex graph patterns. The attribution part is added to this graph part by reverting to the symbolic approach to graph attribution, where attributes are represented symbolically by variables whose possible values are specified by a set of constraints making use of algebraic specifications. Secondly, we extend our refutationally complete tableau-based reasoning method as well as our symbolic model generation approach for graph properties to attributed graph properties. Due to the new logic mentioned above, neatly separating the graph and attribution parts, and the categorical constructions employed only on a more abstract level, we can leave the graph part of the algorithms seemingly unchanged. For the integration of the attribution part into the algorithms, we use an oracle, allowing for flexible adoption of different available SMT solvers in the actual implementation. Finally, our automated reasoning approach for attributed graph properties is implemented in the tool AutoGraph integrating in particular the SMT solver Z3 for the attribute part of the properties. We motivate and illustrate our work with a particular application scenario on graph database query validation.}, language = {en} } @article{SchneiderMaximovaSakizloglouetal.2021, author = {Schneider, Sven and Maximova, Maria and Sakizloglou, Lucas and Giese, Holger}, title = {Formal testing of timed graph transformation systems using metric temporal graph logic}, series = {International journal on software tools for technology transfer}, volume = {23}, journal = {International journal on software tools for technology transfer}, number = {3}, publisher = {Springer}, address = {Heidelberg}, issn = {1433-2779}, doi = {10.1007/s10009-020-00585-w}, pages = {411 -- 488}, year = {2021}, abstract = {Embedded real-time systems generate state sequences where time elapses between state changes. Ensuring that such systems adhere to a provided specification of admissible or desired behavior is essential. Formal model-based testing is often a suitable cost-effective approach. We introduce an extended version of the formalism of symbolic graphs, which encompasses types as well as attributes, for representing states of dynamic systems. Relying on this extension of symbolic graphs, we present a novel formalism of timed graph transformation systems (TGTSs) that supports the model-based development of dynamic real-time systems at an abstract level where possible state changes and delays are specified by graph transformation rules. We then introduce an extended form of the metric temporal graph logic (MTGL) with increased expressiveness to improve the applicability of MTGL for the specification of timed graph sequences generated by a TGTS. Based on the metric temporal operators of MTGL and its built-in graph binding mechanics, we express properties on the structure and attributes of graphs as well as on the occurrence of graphs over time that are related by their inner structure. We provide formal support for checking whether a single generated timed graph sequence adheres to a provided MTGL specification. Relying on this logical foundation, we develop a testing framework for TGTSs that are specified using MTGL. Lastly, we apply this testing framework to a running example by using our prototypical implementation in the tool AutoGraph.}, language = {en} } @article{SchneiderLambersOrejas2021, author = {Schneider, Sven and Lambers, Leen and Orejas, Fernando}, title = {A logic-based incremental approach to graph repair featuring delta preservation}, series = {International journal on software tools for technology transfer : STTT}, volume = {23}, journal = {International journal on software tools for technology transfer : STTT}, number = {3}, publisher = {Springer}, address = {Berlin ; Heidelberg}, issn = {1433-2779}, doi = {10.1007/s10009-020-00584-x}, pages = {369 -- 410}, year = {2021}, abstract = {We introduce a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing graph repairs from which a user may select a graph repair based on non-formalized further requirements. This incremental approach features delta preservation as it allows to restrict the generation of graph repairs to delta-preserving graph repairs, which do not revert the additions and deletions of the most recent consistency-violating graph update. We specify consistency of graphs using the logic of nested graph conditions, which is equivalent to first-order logic on graphs. Technically, the incremental approach encodes if and how the graph under repair satisfies a graph condition using the novel data structure of satisfaction trees, which are adapted incrementally according to the graph updates applied. In addition to the incremental approach, we also present two state-based graph repair algorithms, which restore consistency of a graph independent of the most recent graph update and which generate additional graph repairs using a global perspective on the graph under repair. We evaluate the developed algorithms using our prototypical implementation in the tool AutoGraph and illustrate our incremental approach using a case study from the graph database domain.}, language = {en} }