TY  - JOUR
A1  - Bandyopadhyay, Soumyadip
A1  - Sarkar, Dipankar
A1  - Mandal, Chittaranjan
A1  - Giese, Holger
T1  - Translation validation of coloured Petri net models of programs on integers
JF  - Acta informatica
N2  - Programs are often subjected to significant optimizing and parallelizing transformations based on extensive dependence analysis. Formal validation of such transformations needs modelling paradigms which can capture both control and data dependences in the program vividly. Being value-based with an inherent scope of capturing parallelism, the untimed coloured Petri net (CPN) models, reported in the literature, fit the bill well; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both the source and the transformed codes for translation validation than strictly sequential variable-based IRs like sequential control flow graphs (CFGs). In this work, an efficient path-based equivalence checking method for CPN models of programs on integers is presented. Extensive experimentation has been carried out on several sequential and parallel examples. Complexity and correctness issues have been treated rigorously for the method.
Y1  - 2022
U6  - https://doi.org/10.1007/s00236-022-00419-z
SN  - 0001-5903
SN  - 1432-0525
VL  - 59
IS  - 6
SP  - 725
EP  - 759
PB  - Springer
CY  - New York
ER  - 
TY  - JOUR
A1  - Gabrysiak, Gregor
A1  - Giese, Holger
A1  - Seibel, Andreas
T1  - Towards next generation design thinking : scenario-based prototyping for designing complex software systems with multiple users
Y1  - 2011
SN  - 978-3-642-13756-3
ER  - 
TY  - JOUR
A1  - Gabrysiak, Gregor
A1  - Giese, Holger
A1  - Seibel, Andreas
T1  - Towards next-generation design thinking II : virtual muti-user software prototypes
Y1  - 2012
ER  - 
TY  - GEN
A1  - Giese, Holger
ED  - Kouchnarenko, Olga
ED  - Khosravi, Ramtin
T1  - Formal models and analysis for self-adaptive cyber-physical systems
BT  - (extended abstract)
T2  - Lecture notes in computer science
N2  - In this extended abstract, we will analyze the current challenges for the envisioned Self-Adaptive CPS. In addition, we will outline our results to approach these challenges with SMARTSOS [10] a generic approach based on extensions of graph transformation systems employing open and adaptive collaborations and models at runtime for trustworthy self-adaptation, self-organization, and evolution of the individual systems and the system-of-systems level taking the independent development, operation, management, and evolution of these systems into account.
Y1  - 2017
SN  - 978-3-319-57666-4
SN  - 978-3-319-57665-7
U6  - https://doi.org/10.1007/978-3-319-57666-4_1
SN  - 0302-9743
SN  - 1611-3349
VL  - 10231
SP  - 3
EP  - 9
PB  - Springer
CY  - Cham
ER  - 
TY  - JOUR
A1  - Giese, Holger
A1  - Hildebrandt, Stephan
A1  - Lambers, Leen
T1  - Bridging the gap between formal semantics and implementation of triple graph grammars
JF  - Software and systems modeling
N2  - The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. A prerequisite to verify model transformations at the level of the model transformation specification is that an unambiguous formal semantics exists and that the implementation of the model transformation language adheres to this semantics. However, for existing relational model transformation approaches, it is usually not really clear under which constraints particular implementations really conform to the formal semantics. In this paper, we will bridge this gap for the formal semantics of triple graph grammars (TGG) and an existing efficient implementation. While the formal semantics assumes backtracking and ignores non-determinism, practical implementations do not support backtracking, require rule sets that ensure determinism, and include further optimizations. Therefore, we capture how the considered TGG implementation realizes the transformation by means of operational rules, define required criteria, and show conformance to the formal semantics if these criteria are fulfilled. We further outline how static and runtime checks can be employed to guarantee these criteria.
Y1  - 2014
U6  - https://doi.org/10.1007/s10270-012-0247-y
SN  - 1619-1366
SN  - 1619-1374
VL  - 13
IS  - 1
SP  - 273
EP  - 299
PB  - Springer
CY  - Heidelberg
ER  -