11. 


12. 
 Churchill, Martin, et al.
(författare)

Modular Semantics for Transition System Specifications with Negative Premises
 2013

Ingår i: Proceedings of the 24th International Conference on Concurrency Theory.  Heidelberg : Springer Berlin/Heidelberg.  9783642401831  9783642401848 ; s. 4660

Konferensbidrag (refereegranskat)abstract
 <p>Transition rules with negative premises are needed in the structural operational semantics of programming and specification constructs such as priority and interrupt, as well as in timed extensions of specification languages. The wellknown prooftheoretic semantics for transition system specifications involving such rules is based on wellsupported proofs for closed transitions. Dealing with open formulae by considering all closed instances is inherently nonmodular  proofs are not necessarily preserved by disjoint extensions of the transition system specification. Here, we conservatively extend the notion of wellsupported proof to open transition rules. We prove that the resulting semantics is modular, consistent, and closed under instantiation. Our results provide the foundations for modular notions of bisimulation such that equivalence can be proved with reference only to the relevant rules, without appealing to all existing closed instantiations of terms. © 2013 SpringerVerlag.</p>


13. 
 Cimini, Matteo, et al.
(författare)

Nominal SOS
 2012

Ingår i: Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII).  Amsterdam : Elsevier. ; s. 103116

Konferensbidrag (refereegranskat)abstract
 <p>Plotkin’s style of Structural Operational Semantics (SOS) has become a de facto standard in giving operational semantics to formalisms and process calculi. In many such formalisms and calculi, the concepts of names, variables and binders are essential ingredients. In this paper, we propose a formal framework for dealing with names in SOS. The framework is based on the Nominal Logic of Gabbay and Pitts and hence is called Nominal SOS. We define nominal bisimilarity, an adaptation of the notion of bisimilarity that is aware of binding. We provide evidence of the expressiveness of the framework by formulating the early πcalculus and Abramsky’s lazy λcalculus within Nominal SOS. For both calculi we establish the operational correspondence with the original calculi. Moreover, in the context of the <strong>π</strong>calculus, we prove that nominal bisimilarity coincides with Sangiorgi’s open bisimilarity and in the context of the λcalculus we prove that nominal bisimilarity coincides with Abramsky’s applicative bisimilarity. © 2012 Elsevier B.V.</p>


14. 
 Dechesne, Francien, et al.
(författare)

Interpreted Systems Semantics for Process Algebra with Identity Annotations
 2013

Ingår i: Logic, Language, and Computation : 9th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2011, Kutaisi, Georgia, September 2630, 2011, Revised Selected Papers.  Heidelberg : Springer Berlin/Heidelberg.  9783642369759  9783642369766 ; s. 182205

Bokkapitel (refereegranskat)abstract
 <p>Process algebras have been developed as formalisms for specifying the behavioral aspects of protocols. Interpreted systems have been proposed as a semantic model for multiagent communication. In this paper, we connect these two formalisms by defining an interpreted systems semantics for a generic process algebraic formalism. This allows us to translate and compare the vast body of knowledge and results for each of the two formalisms to the other and perform epistemic reasoning, e.g., using modelchecking tools for interpreted systems, on process algebraic specifications. Based on our translation we formulate and prove some results about the interpreted systems generated by process algebraic specifications. © 2013 SpringerVerlag.</p>


15. 
 Dechesne, Francien, et al.
(författare)

Operational and Epistemic Approaches to Protocol Analysis : Bridging the Gap
 2007

Rapport (övrigt vetenskapligt)abstract
 <p>Operational models of (security) protocols, on one hand, are readable and conveniently match their implementation (at a certain abstraction level). Epistemic models, on the other hand, are appropriate for specifying knowledgerelated properties such as anonymity or secrecy. These two approaches to specification and verification have so far developed in parallel and one has either to define ad hoc correctness criteria for the operational model or use complicated epistemic models to specify the operational behavior. We work towards bridging this gap by proposing a combined framework which allows for modeling the behavior of a protocol in a process language with an operational semantics and supports reasoning about properties expressed in a rich logic which combines temporal and epistemic operators.</p>


16. 
 Fragal, Vanderson Hafemann, et al.
(författare)

Reducing the Concretization Effort in FSMBased Testing of Software Product Lines
 2017

Ingår i: 10th IEEE International Conference on Software Testing, Verification and Validation Workshops  ICSTW 2017.  Los Alamitos, CA : IEEE.  9781509066766  9781509066773 ; s. 329336

Konferensbidrag (refereegranskat)abstract
 <p>To test a Software Product Line (SPL), the test artifacts and the techniques must be extended to support variability. In general, when new SPL products are developed, more tests are generated to cover new or modified features. A dominant source of extra effort for such tests is the concretization of newly generated tests. Thus, minimizing the amount of new nonconcretized tests required to perform conformance testing on new products reduces the overall test effort. In this paper, we propose a test reuse strategy for conformance testing of SPL products that aims at reducing test effort. We use incremental test generation methods based on finite state machines (FSMs) to maximize test reuse. We combine these methods with a selection algorithm used to identify nonredundant concretized tests. We illustrate our strategy using examples and a case study with an embedded mobile SPL. The results indicate that our strategy can save up to 36% of test effort in comparison to current test reuse strategies for the same fault detection capability. © 2017 IEEE.</p>


17. 
 Gebler, Daniel, et al.
(författare)

Algebraic MetaTheory of Processes with Data
 2013

Ingår i: Proceedings Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics.  Open Publishing Association. ; s. 6377

Konferensbidrag (refereegranskat)abstract
 <p>There exists a rich literature of rule formats guaranteeing different algebraic properties for formalisms with a Structural Operational Semantics. Moreover, there exist a few approaches for automatically deriving axiomatizations characterizing strong bisimilarity of processes. To our knowledge, this literature has never been extended to the setting with data (e.g. to model storage and memory). We show how the rule formats for algebraic properties can be exploited in a genericmanner in the setting with data. Moreover, we introduce a new approach for deriving sound and groundcomplete axiom schemata for a notion of bisimilarity with data, called stateless bisimilarity, based on intuitive auxiliary function symbols for handling the store component. We do restrict, however, the axiomatization to the setting where the store component is only given in terms of constants. © Gebler, Goriac & Mousavi.</p>


18. 


19. 


20. 
 Hafemann Fragal, Vanderson, 1988
(författare)

Automatic generation of configurable testsuites for software product lines
 2018

Doktorsavhandling (övrigt vetenskapligt)abstract
 <p>Software Product Line Engineering (SPLE) is an approach used in the development of similar products, which aims at systematic reuse of software artifacts. The SPLE process has several activities executed to assure software quality. Quality assurance is of vital importance for achieving and maintaining a high quality for various artifacts, such as products and processes. Testing activities are widely used in industry for quality assurance. However, the effort for applying testing is usually high, and increasing the testing efficiency is a major concern. A common means of increasing efficiency is automation of test design. Several techniques, processes, and strategies were developed for SPLE testing, but still many problems are open in this area of research. The challenge in focus is the reduction of the overall test effort required to test SPLE products. Test effort can be reduced by maximizing test reuse using models that take advantage of the similarity between products. The thesis goal is to automate the generation of small testsuites with high fault detection and low test redundancy between products. To achieve the goal, equivalent tests are identified for a set of products using complete and configurable testsuites. Two research directions are explored, one is productbased centered, and the other is product linecentered. For test design, testsuites that have full fault coverage were generated from state machines with and without feature constraints. A prototype tool was implemented for test design automation. In addition, the proposed approach was evaluated using examples, experimental studies, and an industrial case study for the automotive domain. The results of the productbased centered approach indicate a reduction of 36% on the number of test cases that need to be concretized. The results of the product linecentered approach indicate a reduction of 50% on the number of test cases generated for groups of product configurations.</p>

