39 research outputs found
Timing diagrams requirements modeling using Event-B formal methods
No full textTiming diagrams provide an intuitive graphical specification for time constraints and causal dependencies between a system’s objects. Such a view can provide useful insight during Requirements Engineering (RE). Formal Modeling techniques allow abstract system level models to be explored in revealing detail and provide feedback via verification and validation methods such as proofs of consistency, model checking and animation. Here, we bring these two modelling approaches together. In particular we present techniques to extend a graphical modeling capability for formal modeling into the real-time domain by developing a Timing diagram view for the Event-B formal method and its graphical front-end, UML-B. Translation schemes to Event-B and UML-B are proposed and presented. A case study of a lift system is used to demonstrate the translation in practice
Engineering and theoretical underpinnings of retrenchment
No full textRefinement is reviewed, highlighting in particular the distinction between its use as a specification constructor at a high level, and its use as an implementation mechanism at a low level. Some of its shortcomings as a specification constructor at high levels of abstraction are pointed out, and these are used to motivate the adoption of retrenchment for certain high level development steps. Basic properties of retrenchment are described, including a justification of the operation proof obligation, simple examples, its use in requirements engineering and model evolution, and simulation properties. The interaction of retrenchment with refinement notions of correctness is overviewed, as is a range of other technical issues. Two case study scenarios are presented. One is a simple digital redesign control theory problem, and the other is an overview of the application of retrenchment to the Mondex Purse development
JCSProB: Implementing Integrated Formal Specifications in Concurrent Java
No full textThe ProB model checker provides tool support for an integrated formal specification approach, which combines the classical state-based B language with the event-based process algebra CSP. In this paper, we present a developing strategy for implementing such a combined ProB specification as a concurrent Java program. A Java implementation of the combined B and CSP model has been developed using a similar approach to JCSP. A set of translation rules relates the formal model to its Java implementation, and we also provide a translation tool JCSProB to automatically generate a Java program from a ProB specification. To demonstrate and exercise the tool, several B/CSP models, varying both in syntactic structure and behavioural/concurrency properties, are translated by the tool. The models manifest the presence and absence of various safety, deadlock, and bounded fairness properties; the generated Java code is shown to faithfully reproduce them. Run-time safety and bounded fairness checking is also demonstrated. The Java programs are discussed to demonstrate our implementation of the abstract B/CSP concurrency model in Java. In conclusion we consider the effectiveness and generality of the implementation strategy
Retrenchment: Extending the Reach of Refinement
No full textDiscussion of a simple example demonstrates various expressive limitations of the refinement calculus, and suggests a liberalization of refinement, called retrenchment, which will support an analogous formal development calculus. Useful concrete system behaviour can be specified outside the domain of pure refinement, and a case is made for fluidity between I/O and state components across the development step. A syntax and a formal definition are presented for retrenchment, which has some necessary properties for a formal development calculus: transitivity gives stepwise composition of retrenchments, and monotonicity w.r.t. the specification language constructors gives piecewise construction of retrenchments. 1 Introduction and r esum e of B From early concerns about proving correctness of programs such as Hoare's [19] and Dijkstra's [15], a mature refinement calculus of specifications to programs has developed. This development has been in two strands, the predicate transformer/ lattic..
Recommended from our members
Automated categorisation of e-journals by synonym analysis of n-grams
No full textAutomatic keyword or keyphrase extraction is concerned with assigning keyphrases to documents based on words from within the document. Previous studies have shown that in a significant number of cases author-supplied keywords are not appropriate for the document to which they are attached. This can either be because they represent what the author believes a paper is about not what it actually is, or because they include keyphrases which are more classificatory than explanatory e.g., “University of Poppleton” instead of “Knowledge Discovery in Databases”. Thus, there is a need for a system that can generate an appropriate and diverse range of keyphrases that reflect the document. This paper proposes two possible solutions that examine the synonyms of words and phrases in the document to find the underlying themes, and presents these as appropriate keyphrases. Using three different freely available thesauri, the work undertaken examines two different methods of producing keywords and compares the outcomes across multiple strands in the timeline. The primary method explores taking n-grams of the source document phrases, and examining the synonyms of these, while the secondary considers grouping outputs by their synonyms. The experiments undertaken show the primary method produces good results and that the secondary method produces both good results and potential for future work. In addition, the different qualities of the thesauri are examined and it is concluded that the more entries in a thesaurus, the better it is likely to perform. The age of the thesaurus or the size of each entry does not correlate to performance
Recommended from our members
Keyphrase extraction by synonym analysis of n-grams for e-journals categorisation
No full textAutomatic keyword or keyphrase extraction is concerned with assigning keyphrases to documents based on words from within the document. Previous studies have shown that in a significant number of cases author-supplied keywords are not appropriate for the document to which they are attached. This can either be because they represent what the author believes the paper is about not what it actually is, or because they include keyphrases which are more classificatory than explanatory e.g., “University of Poppleton” instead of “Knowledge Discovery in Databases”. Thus, there is a need for a system that can generate appropriate and diverse range of keyphrases that reflect the document. This paper proposes a solution that examines the synonyms of words and phrases in the document to find the underlying themes, and presents these as appropriate keyphrases. The primary method explores taking n-grams of the source document phrases, and examining the synonyms of these, while the secondary considers grouping outputs by their synonyms. The experiments undertaken show the primary method produces good results and that the secondary method produces both good results and potential for future work
The nature, causes and consequences of harm in emotionally-demanding occupations
No full textTraditional approaches to understanding psychosocial job characteristics and well-being have been quite general in that they explore links between general job characteristics such as workload and control on workers in many different sorts of occupations. One example of a more specific approach can be found in research into emotional labour - the requirement to regulate both feelings and the expression of feelings for organizational goals. Early research into emotional labour focused on customer service workers (CSW) but has more recently also considered human service workers (HSW) such as nurses and social workers. A more specific approach to thinking about the outcomes of demanding psychosocial job characteristics can be found in research on burnout which is thought to have three elements: emotional exhaustion, depersonalization (also labelled cynicism), and (low) accomplishment (also called professional efficacy). Much recent research has started to explore the links between emotional demands and burnout. The main aim of this project is therefore to explore the nature of such links through undertaking three distinct tasks. The first is a literature review of evidence and theory while the second two tasks comprise two empirical studies examining several key issues in burnout research.
This report and the work it describes were funded by the Health and Safety Executive (HSE). Its contents, including any opinions and/or conclusions expressed, are those of the author alone and do not necessarily reflect HSE policy
