The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Offshore outsourcing has become a cost-saving measure in modern software businesses. However, there are numerous risks associated in this business model. Among these risks, "mum effect" could be one of the serious threats to software development projects. This paper extends our previous work on the perceived probability of "mum effect" in offshore outsourcing scenarios based on...
Summary form only given. In software testing, when testing samples contradict the specification of a software system, the best way to locate the error-making commands is logical reasoning; therefore a formal logical reasoning system might be developed for making revision of software systems. In this paper, a formal system, called R-calculus, is introduced in first order languages. It is used to spot...
Soon after the birth of the flourishing research area of model checking in the early eighties, researchers started to apply this technique to finite automata equipped with probabilities. The initial focus was on qualitative properties - e.g., does a program terminate with probability one? - but later efficient algorithms were developed for quantitative questions as well. Model checking of probabilistic...
Symmetry reduction holds great promise to counter the state explosion problem. However, currently it is "conducting a life on the fringe ", and is not widely applied, mainly due to the restricted applicability of many of the techniques. In this paper we propose a symmetry reduction technique applied to high-level formal specification languages (B and Z). Not only does symmetry arise naturally...
PSL is a kind of temporal logic which uses SEREs as additional formula constructs. We present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. In this paper, we extend the LTL symbolic model checking algorithm to that of APSL, and present a tableau based APSL verification approach. Moreover, we show how to implement this...
This paper investigates a complete axiomatic system for propositional projection temporal logic (PPTL). To this end, the syntax, semantics, and logic laws of PPTL are briefly introduced. Further, the normal form of PPTL formulas is presented. Moreover, an axiomatic system of PPTL is formalized. A set of axioms and inference rules are given in details. To assist the proof within the system, some theorems...
Requirements changes can occur both during and after a phase of development. It is difficult and intensive work to integrate requirements changes made after specification is completed. Sequence-based specification was developed to convert ordinary functional requirements into complete, consistent, and traceably correct specifications through a constructive process. Algorithms for managing requirements...
Confined separation logic is a new extension to separation logic designed to deal with problems involving dangling references within shared mutable structures. In particular, it allows for reasoning about confinement in object-oriented programs. In this paper, we discuss the semantics of such an extension by defining a relational model for the overall logic, parametric on the shapes of both the store...
To ensure the requested quality of Web applications as expected, it is critical and challenging to test them. This work defines Web application schema and constructs Web application relation graph in order to model Web applications. An approach to generating test paths is presented by establishing path-generating graph which is derived from the Web application relation graph and used to produce path...
Preference logic programming (PLP) is an extension of constraint logic programming for declaratively specifying problems requiring optimization or comparison and selection among alternative solutions to a query. PLP essentially separates the programming of a problem itself from the criteria specification of its optimal solutions. The main challenge to implement a PLP system is that how the defined...
In this paper, we propose a fine-grained coupling metrics suite for aspect-oriented (AO) systems, to measure software changes during system evolution. We also present a correlation model in terms of intermediate processes, for better evaluating the relation between coupling metrics and system maintainability. To investigate the practicability of our proposed model, we have implemented a coupling metrics...
We present a thorough study of propositional dynamic logic over a variation of labeled transition systems, called accelerated labelled transition systems, which are transition systems labeled with regular expressions over action labels. We study the model checking and satisfiability decision problems. Through a notion of regular expression rewriting, we reduce these two problems to the corresponding...
So far, many nonmonotonic logics are available to deal with the problem of reasoning about completeness, consistency and priorities of the knowledge. The two representative formalisms of them are default reasoning and belief revision, on which the frameworks of Brewka's default theories and Rodrigues' structured clusters are based, respectively. In this paper, we present a framework with the meta-formalism...
Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, not a trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.