An IDE to Build and Check Task Flow Models

This paper presents the Eclipse plug-ins for the Task Flow model in the Discovery Method. These plug-ins provide an IDE for the Task Algebra compiler and the model-checking tools. The Task Algebra is the formal representation for the Task Model and
of 11
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
    a  r   X   i  v  :   1   1   0   7 .   2   6   8   3  v   1   [  c  s .   S   E   ]   1   3   J  u   l   2   0   1   1 An IDE to Build and Check Task Flow Models Carlos Alberto Fernandez-y-Fernandez 1 , Jose Angel Quintanar Morales 2 , andHermenegildo Fernandez Santos 2 1 Instituto de Computaci´on, Universidad Tecnol´ogica de la Mixteca, M´exico 2 Lab. de Inv. y Des. en Ing. de Soft., Universidad Tecnol´ogica de la Mixteca, M´exico { caff, joseangel, ps2010160001 } Abstract.  This paper presents the Eclipse plug-ins for the Task Flowmodel in the Discovery Method. These plug-ins provide an IDE for theTask Algebra compiler and the model-checking tools. The Task Algebrais the formal representation for the Task Model and it is based on simpleand compound tasks. The model-checking techniques were developed tovalidate Task Models represented in the algebra. Keywords:  lightweightformal specification; software modelling; model-checking. 1 Introduction There has been a steady take up in the use of formal calculi for software con-struction over the last 25 years [1], but mainly in academia. Although there aresome accounts of their use in industry (basically in critical systems), the major-ity of software houses in the “real world” have preferred to use visual modellingas a kind of “semi-formal” representation of software. A method is consideredformal if it has well-defined mathematical basis. Formal methods provide a syn-tactic domain (i.e., the notation or set of symbols for use in the method), asemantic domain (like its universe of objects), and a set of precise rules defininghow an object can satisfy a specification [11]. In addition, a specification is a setof sentences built using the notation of the syntactic domain and it representsa subset of the semantic domain. Spivey says that formal methods are based onmathematical notations and “they describe what the system must do withoutsaying how it is to be done” [10], which applies to the non-constructive approachonly. Mathematical notations commonly have three characteristics: –  conciseness - they represent complex facts of a system in a brief space; –  precision - they can specify exactly everything that is intended; –  unambiguity - they do not admit multiple or conflicting interpretations.Essentially, a formal method can be applied to support the development of soft-ware and hardware. This paper shows an IDE for modelling and checking taskflow models using a particular process algebra, called Task Algebra, to charac-terise the Task Flow models in the Discovery Method. The advantage is that thiswill allow software engineers to use diagram-based design methods that have asecure formal underpinning.  1.1 The Discovery Method The Discovery Method is an object-oriented methodology proposed formally in1998 by Simons [8,9]; it is considered by the author to be a method focusedmostly on the technical process. The Discovery Method is organised into fourphases; Business Modelling, Object Modelling, System Modelling, and SoftwareModelling (Simons, pers. comm.).The Business Modelling phase is task-oriented.A task is defined in the Discovery Method as something that “has the specificsense of an activity carried out by stakeholders that has a business purpose” (Si-mons, pers. comm.). This task-based exploration will lead eventually towards thetwo kinds of Task Diagrams: The Task Structure and Task Flow Diagrams. Theworkflow is represented in the Discovery Method using the Task Flow Diagram.It depicts the order in which the tasks are realised in the business, expressingalso the logical dependency between tasks. While the notation used in the Dis-covery Method is largely based on the Activity Diagram of UML, it maintainsconsistently the labelled ellipse notations for tasks. 1.2 The Task Flow models Even though Task Flow models could be represented using one of the processalgebras described above, a particular algebra was defined with the aim of havinga clearer translation between the graphical model and the algebra. One of themain difficulties with applying an existing process algebra was the notion thatprocesses consist of atomic steps, which can be interleaved. This is not the casein the Task Algebra, where even simple tasks have a non-atomic duration andare therefore treated as intervals, rather than atomic events. A simple task inthe Discovery Method [8] is the smallest unit of work with a business goal. Asimple task is the minimal representation of a task in the model. A compoundtask can be formed by either simple or compound tasks in combination withoperators defining the structure of the Task Flow Model. In addition to simpletasks and compound tasks, the abstract syntax also requires the definition of three instantaneous events. These may form part of a compound task in theabstract syntax. 2 The Task Flow metamodel 2.1 The Task Algebra for Task Flow models The basic elements of the abstract syntax are: the simple task, which is definedusing a unique name to distinguish it from others;  ε  representing the emptyactivity; and the success  σ  and failure  ϕ  symbols, representing a finished activity.Simple and compound tasks are combined using the operators that build up thestructures allowed in the Task Flow Model. The basic syntax structures for theTask Flow Model are sequential composition, selection, parallel composition,repetition, and encapsulation. The algebra definition is shown in table 1.  Activity  ::=  ε  – empty activity | σ  – succeed | ϕ  – fail | Task  – a single task | Activity ; Activity  – a sequence of activity | Activity  +  Activity  – a selection of activity | Activity    Activity  – parallel activity | µx. ( Activity ; ε  +  x ) – until-loop activity | µx. ( ε  +  Activity ; x ) – while-loop activity Task  ::=  Simple  – a simple task | Activity  – encapsulated activity Table 1.  abstract syntax definition A task can be either a simple or a compound task. Compound tasks aredefined between brackets ’ { ’ and ’ } ’, and this is also called encapsulation becauseit introduces a different context for the execution of the structure inside it. Curlybrackets are used in the syntax context to represent diagrams and sub-diagramsbut also have implications for the semantics. Also, parentheses can be used tohelp comprehension or to change the associativity of the expressions. Expressionsassociate to the right by default. More details of the axioms can be seen in [6]. 2.2 Model-checking A set of traces is the trace semantic representation for a Task Flow Diagram.The verification of the diagram may be made in different ways. The simplestoperations could be performed by set operators but more operations may be ap-plied over the traces using temporal logic. Temporal logic has being extensivelyapplied with specification and verification of software. The set of traces, obtainedfrom a task algebra expression, may be used to verify some temporal and logicalproperties within the specification expressed by the diagrams. For this reason, asimple implementation of LTL was built. This LTL implementation works overthe trace semantics generated from a Task Algebra expression. Because the tracesemantics represent every possible path of the Task Flow diagram expressed inthe Task Algebra, it is straightforward to use LTL formulas to quantify univer-sally over all those paths. In this section, some examples using Linear TemporalLogic (LTL) are presented, to illustrate the reasoning capabilities of the LTLmodule. LTL is a temporal logic, formed adding temporal operators to the pred-icate calculus. These operators that can be used to refer to future states with noquantification over paths. In addition, a CTL application was built to test CTLtheorems against expressions in the task algebra. In this case, the applicationhas to transform the traces in a tree representation before applying the expres-sion. While LTL formulas express temporal properties over all undifferentiatedpaths, Computational Tree Logic (CTL) also considers quantification over setsof paths. CTL is a branching-time logic [5] and theorems in this logic may also  be tested against a set of traces obtained from a task algebra expression, in thesame way that LTL theorems were tested above. 3 A tool for formal specification of Task Flow models 3.1 Analysis of Integrated Development Environments (IDE) Through a search in surveys and articles published in digital media, Eclipse ischosen as the top two open source IDEs best positioned among developers. How-ever, Eclipse showed a better performance due to the existence of robust toolsfor the development of plug-in, as it has with the Plug-in’s Development Envi-ronment (PDE) which provides tools to create, develop, test, debug, build anddeploy Eclipse plug-ins, modules and features to update the sites and productsRiched Client Platform (RCP). PDE consists of three elements: –  PDE User Interface (UI) for designing the user interface; –  PDE Tools Application Programming Interface (API Tooling) useful piecesof code to develop applications; –  PDE Builder (Build), manager responsible for the administration of the plug-in.Besides all this, the GMF frameworks(Graphic Modeling Framework - Frame-work for graphic editing) and Eclipse Modeling Framework (Eclipse ModelingFramework, EMF), which facilitate the construction. We can get a highly func-tional visual editor using EMF to build a structured data model enriched byGMF editors. The main advantage is that being all development based on build-ing a structured model, the time spent on the maintenance phase will be sub-stantially reduced. 3.2 The architecture of the task model tool As mentioned above, our general architecture is based on the Eclipse framework.The first component is able to model Task Flow diagrams and translate them intoa metamodel formed by Task Algebra expressions. The resultant file containingthe metamodel is used by the Task Algebra compiler in order to generate thetrace semantics.In addition, the other component in Eclipse has the responsibility to receiveLTL and CTL queries. The queries are sent to the relevant model-checking tool.Textual results are returned by the tool and have to be interpreted by LTL/CTLEclipse plugin. Figure 1 shows the general dependency between the componentsof our project. 4 Formal modelling made easy 4.1 Design of the structured model Once identified the use cases, classes were designed including the interactionbetween different objects of the tool, we then proceeded to design the structured  Fig.1.  Architecture of the Task Model Tool. model. This model is presented in Figure 2. All development of the structuredmodel is based on the use case diagram, when we should be extra careful as itmigrates from an abstract model such as use cases and results in a diagram fromwhich one has the possibility of building the computer application as such, in thiscase, set the application logic. Note that only cover part of the user interaction. Fig.2.  Class model for the Task model plug-in,based on GMF. 4.2 Development of the graphical model When the structured model is designed properly [2,3], this can be transformedto the model graph. The model is a set of classes that represent real-world in-formation. In our case, the components which are integrated with diagrams. For
Similar documents
View more...
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks

We need your sign to support Project to invent "SMART AND CONTROLLABLE REFLECTIVE BALLOONS" to cover the Sun and Save Our Earth.

More details...

Sign Now!

We are very appreciated for your Prompt Action!