Process patterns allow the modular modelling and adaptable application of business processes. Present descriptions of process patterns show defects like non-uniform and unequivocal description forms and missing relationship definitions. These defects disadvantageously affect the effective usage of process patterns. In this work we introduce the language PROPEL (Process Pattern Description Language), which provides concepts for the semiformal description of process patterns and relationships between process patterns. With the help of PROPEL single process patterns can be modelled and, by definition of relationships, be composed to more complicated processes. With the representation of different views of a process pattern catalog the process patterns and their relationships can be shown clearly. An example illustrates how a process pattern catalog and the contained process patterns are modelled. It is shown that in applying PROPEL the complexity of a process model can be reduced and inconsistencies of processes be eliminated.

Formal specifications are mathematically based techniques with which a system can be analyzed, and its functionalities be described. Case studies have shown that using formal specifications can help reduce bugs and other inconsistencies when implementing a complex system; they are more likely found during the software design phase rather than later. During the process of porting code, testing has been used to verify that the port has the same functionalities as the original. However, testing alone has been deemed necessary but not sufficient to accomplish this. This thesis questions if formal specifications could be used during the process of porting code to create an accurate model of the system, and thereby provide higher degrees of certainty that the final product conforms to the original. A step-by-step methodology is presented to answer this question. The methodology ascertains the behavior of a port target through testing and a formal specification model based on these tests is created. This model is then used to create the port. The result indicates that the methodology used has some potential since it provided a high level of certainty that the ported code adhered to the original. Since the methodology puts a high emphasis on the specification and has several layers of verification, it is likely that it is suitable for projects with several modules and interdependencies. When using it for porting a trivial or non-complex system, the overhead of the methodology may prove high in comparison to the value gained. It was also found that one must take into consideration the implicit functionalities a language provides. Strict reliance on a model could thereby lead to a less flexible process where creativity and consideration of the specifics of the target language may have produced a different result. / Formella specifikationer är matematiska tekniker med vilka ett system kan analyseras och dess funktioner beskrivas. Fallstudier har visat att användning av formella specifikationer vid mjukvaruutveckling kan bidra till att reducera antalet fel och därmed minska omkostnaderna. Vid portering av kod har tester använts för att verifiera att porteringen har samma funktionaliteter som originalet. Tester anses dock vara otillräckliga - om än nödvändiga - för att fullständigt beskriva ett system. Denna avhandling ställer frågan om formella specifikationer kan användas i en porteringsprocess och därmed ge en högre grad av tillförlitlighet i att porteringen överensstämmer med originalet. En steg-för-steg-metodik presenteras för att besvara denna fråga. Metodiken använder sig av tester för att beskriva det system som skall porteras och en modell baserad på formella specifikationer skapas genom dessa tester. Denna modell används därefter för att skapa porteringen. Resultatet indikerar att metoden har viss potential eftersom den upplevdes öka förståelsen för referensarbetet och därmed också tryggheten i att den portade koden överensstämde med originalet. Eftersom metodiken lägger stor vikt vid specifikationen och består av flera lager av verifiering är det troligt att den är mer lämplig för system som består av flertalet moduler med inbördes beroende. Vid användning för att portera ett trivialt system kan metodens om-kostnader visa sig vara för höga i förhållande till det värde som erhålls. Det visade sig även att en porteringsprocess måste ta hänsyn till de implicita funktioner ett språk tillhandahåller. En strikt anpassning till en modell kan därmed leda till en mindre flexibel process och därmed leda till ett icke tillfredsställande resultat, där kreativitet och hänsyn till målspråket skulle kunna ha gett ett annat.

In recent years, there has been a ood of continuously changing information from a variety of web resources such as web databases, web sites, web services and programs. Online Social Networks (OSNs) represent such a eld where huge amounts of information are being posted online over time. Due to the nature of OSNs, which o er a productive source for qualitative and quantitative personal information, researchers from various disciplines contribute to developing methods for extracting data from OSNs. However, there is limited research which addresses extracting data automatically. To the best of the author's knowledge, there is no research which focuses on tracking the real time changes of information retrieved from OSN pro les over time and this motivated the present work. This thesis presents di erent approaches for automated Data Extraction (DE) from OSN: crawler, parser, Multi Agent System (MAS) and Application Programming Interface (API). Initially, a parser was implemented as a centralized system to traverse the OSN graph and extract the pro- le's attributes and list of friends from Myspace, the top OSN at that time, by parsing the Myspace pro les and extracting the relevant tokens from the parsed HTML source les. A Breadth First Search (BFS) algorithm was used to travel across the generated OSN friendship graph in order to select the next pro le for parsing. The approach was implemented and tested on two types of friends: top friends and all friends. In case of top friends, 500 seed pro les have been visited; 298 public pro les were parsed to get 2197 top friends pro les and 2747 friendship edges, while in case of all friends, 250 public pro les have been parsed to extract 10,196 friends' pro les and 17,223 friendship edges. This approach has two main limitations. The system is designed as a centralized system that controlled and retrieved information of each user's pro le just once. This means that the extraction process will stop if the system fails to process one of the pro les; either the seed pro le ( rst pro le to be crawled) or its friends. To overcome this problem, an Online Social Network Retrieval System (OSNRS) is proposed to decentralize the DE process from OSN through using MAS. The novelty of OSNRS is its ability to monitor pro les continuously over time. The second challenge is that the parser had to be modi ed to cope with changes in the pro les' structure. To overcome this problem, the proposed OSNRS is improved through use of an API tool to enable OSNRS agents to obtain the required elds of an OSN pro le despite modi cations in the representation of the pro le's source web pages. The experimental work shows that using API and MAS simpli es and speeds up the process of tracking a pro le's history. It also helps security personnel, parents, guardians, social workers and marketers in understanding the dynamic behaviour of OSN users. This thesis proposes solutions for web database processing on data extraction from OSNs by the use of parser and MAS and discusses the limitations and improvements. / Taibah University

<p>Formal methods such as Event-B are a widely used approach for developing critical systems. This thesis demonstrates that creating models and proving the consistency of the models at the requirements level during software (system) development is an effective way to reduce the occurrence of faults and errors in a practical application. An insulin infusion pump (IIP) is a complicated and time critical system. This thesis uses Event-B to specify models for an IIP, based on a draft requirements document developed by the US Food and Drug Administration (FDA). Consequently it demonstrates Event-B can be used effectively to detect the missing properties, the missing quantities, the faults and the errors at the requirements level of a system development. The IIP is an active and reactive time control system. To achieve the goal of handling timing issues in the IIP system, we made extensions of an existing time pattern specified using Event-B to enrich the semantics of the Event-B language. We created several sets to model the activation times of different events and the union of these time sets defines a global time activation set. The tick of global time is specified as a progress tick event. All the actions in an event are triggered only when the global time in the time tick event matches the time specified in the event. Time is deleted from the corresponding time set, but not the corresponding global time set while the event is triggered. A time point is deleted from the global time set only when there are no pending actions for that time point. Through discharging proof obligations using Event-B, we achieved our goal of improving the requirements document.</p> / Master of Computer Science (MCS)

The specification of enterprise information systems using formal specification languages enables the formal verification of these systems. Reasoning about the properties of a formal specification is a tedious task that can be facilitated much through the use of an automated reasoner. However, set theory is a corner stone of many formal specification languages and poses demanding challenges to automated reasoners. To this end a number of heuristics has been developed to aid the Otter theorem prover in finding short proofs for set-theoretic problems. This dissertation investigates the applicability of these heuristics to next generation theorem provers. / Computing / M.Sc. (Computer Science)

La sécurité des systèmes d'information devient un enjeu préoccupant pour les organisations tant publiques que privées, car de tels systèmes sont pour la plupart universellement accessibles à partir de navigateurs Web. Parmi tous les aspects liés à la sécurité des systèmes d'information, c'est celui de la sécurité fonctionnelle qui est étudié dans cette thèse sous l'angle de la mise en œuvre de politiques de contrôle d'accès dans une architecture orientée services. L'élément de base de la solution proposée est un modèle générique qui introduit les concepts essentiels pour la conception de gestionnaires d'exécution de politiques de contrôle d'accès et qui établit une séparation nette entre le système d'information et les mécanismes de contrôle d'accès. L'instanciation de ce modèle conduit à un cadre d'applications qui comporte, entre autres, un filtre de contrôle d'accès dynamique. Cette thèse présente également deux méthodes systématiques d'implémentation de ce filtre à partir de politiques écrites en ASTD, une notation graphique formelle basée sur les statecharts augmentés d'opérateurs d'une algèbre de processus. La notation ASTD est plus expressive que la norme RBAC et ses extensions, la solution actuellement privilégiée dans l'industrie. La première méthode repose sur une transformation de politiques de contrôle d'accès, instanciées à partir de patrons de base exprimés en ASTD, en des processus BPEL. La deuxième méthode est basée sur une interprétation de spécifications ASTD par des processus BPEL. Dans les deux cas, les processus BPEL s'exécutent dans un moteur d'exécution BPEL et interagissent avec le système d'information. Ces deux méthodes permettent une implémentation automatique d'un cadre d'applications à partir de la spécification de départ. Finalement, un prototype a été réalisé pour chacune des deux méthodes afin de montrer leur faisabilité au niveau fonctionnel et de comparer leurs performances au niveau système / Nowadays information systems are, more than ever, available through Web browsers. Therefore, they become vulnerable against attack, which has made security an important issue for public and private organizations. This thesis examines in depth one aspect of information system security, namely functional security through access-control policy enforcement, when such systems are implemented in a service-oriented architecture framework. The foundation of the proposed solution is a generic model that introduces essential concepts to design enforcement managers for access-control policies and clearly separates responsibilities between the information system and access control mechanisms. Instantiation of this model results in a general framework, which encompasses many components including a dynamic access-control filter. This thesis also presents two systematic implementation methods for the dynamic access-control filter from policies expressed in ASTD, a formal and graphical notation based on statecharts enriched with process algebra operators. The ASTD notation is more expressive than the RBAC standard and its extensions, the widely used solution in software engineering. The first method is based on the transformation of access-control policies, instantiated from ASTD patterns, into BPEL processes. The second method is based on the interpretation of ASTD specifications by BPEL processes. In these two cases, the BPEL processes are deployed and executed in a BPEL engine, and interact with the information system. Both methods allow for automatic implementation of an enforcement framework from the initial specification. Finally, prototypes have been developed to illustrate both methods and show their feasibility at the functional level and their performance

Especificações formais são úteis para descrever o que um sistema deve fazer sem definir como, e, em virtude da sua natureza formal e da possibilidade de abstração, é possível analisá-las sistematicamente. No entanto, o uso de especificações formais como parte do desenvolvimento de software não constitui prática comum. Isso se dá, em parte, pelo fato de existirem apenas um pequeno número de metodologias e ferramentas adequadas que dêem suporte a esse desenvolvimento. O primeiro objetivo deste trabalho é propor uma metodologia de desenvolvimento que possibilite, a partir de uma especificação formal em notação Z, produzir uma implementação dessa especificação em Java. Essa metodologia centra-se na geração do esqueleto da aplicação Java e na instrumentação desse esqueleto com mecanismos de verificação de condições (invariantes, pré e pós-condições) e rastreamento de violações dessas condições. Através desses mecanismos, possibilita-se intercalar desenvolvimento formal e informal no processo global de desenvolvimento de software. O segundo objetivo é desenvolver uma ferramenta que implemente parte dessa metodologia, produzindo uma implementação parcial que deverá ser complementada pelo usuário. / Formal specifications are useful for describing what a system should do, without defining how, and, owing to its formal nature, it is possible to analyse them systematically. However useful formal specifications are, their usage as part of the software development process is rather rare. This is, in part, due to the scarcity of both methodologies and tools that support this development. The first goal of this work is to define a software development methodology that enables the developer to produce a Java application from a formal specification written in Z. This methodology will rely strongly on the generation of Java application skeletons and instrumentation of the generated code with means of verifying conditions (invariants, pre and post-conditions) e tracing violations of these conditions. Through this mechanisms, it is possible to mix formal and informal development in the global software development process. The second goal of this work is to develop a tool that will implement part of this methodology, producing a partial implementation that must be complemented by the developer.

A definição de requisitos tem sido reconhecida como uma das mais críticas e difíceis tarefas em engenharia de software. A necessidade de ferramentas de suporte é essencial. Nos dias de hoje, entre os vários métodos existentes para apoiar a fase de requisitos, destaca-se o SADT (Structured Analysis and Design Techniques) devido a sua capacidade de representar modelos. Este trabalho estabelece semântica para o método SADT, baseando-se na inter-relação do método aos sistemas de fluxo de dados (redes, grafos e máquinas de fluxo). Faz-se, inicialmente, uma abordagem operacional para a semântica de seus construtos básicos e, posteriormente discute-se a possibilidade de executar especificações através de simulação. Uma ferramenta para suportar o método SADT foi projetada e construída e é apresentada. Ela foi definida a partir de um modelo, denotado por uma classe, através de uma sintaxe abstrata. Essa ferramenta foi implementada no ambiente PROSOFT, fornecendo para o usuário mais de quarenta operações de apoio a construção/manipulação de diagramas. O trabalho também apresenta a especificação formal em VDM - Vienna Development Method, da semântica dos principais construtos do método SADT, bem como uma proposição de execução de especificações através de simulação são ainda indicadas direções nas quais o trabalho pode ser estendido. / The definition of systems requirements has been known as one of the most critical and dificult tasks as far as the software engineering is concerned. The need support is essential. Nowadays, among the various methods devised to support the phase of requirements, a special emphasis is given to the SADT method (Structured Analysis and Design Techniques), due to its capability of representing models. This work set semantic for the SADT method, based primarily upon the interrelation of the method to the systems of dataflow (nets, graphs and dataflow machines). It deals with an approach of operational semantics to its basic constructs, and it will, afterwards, discuss the possibility of carry out specifications by simulation. A tool was built to support the SADT method, and it was defined by a model denoted by a class, through an abstract syntax. This tool was implemented in the PROSOFT environment, providing for the user, more than forty support operations for the construction /manipulation of diagrams. This work also presents the formal specification of the semantics of the main constructs of the SADT method in VDM - Vienna Development Method; as well as an execution proposal of specifications through simulation. Directions have been indicated concerning the extension of the research.

Currently, the bulk of applications of Formal Concept Analysis (FCA) in software engineering have focussed on software maintenance and re-engineering. In this thesis we broaden the approach by applying FCA to a number of early-phase activities within the software engineering life-cycle. With respect to the requirements engineering phase, a case study is presented comparing two class hierarchies that model aspects of a mass-transit railway ticketing system. The first hierarchy was produced for an existing Object-Z specification of the system while the second was derived using FCA. Contrasting the two hierarchies revealed that they were essentially the same, however, the differences highlighted specification artefacts in the existing hierarchy. With respect to the design phase, the thesis discusses the use of FCA for the navigation and visualisation of Formal Specifications written in Z. In response to the continued call for formal methods tool support, we implement and explore a prototype specification browser that exploits the abstractions afforded by FCA. The research hypothesis is an integrated architecture for navigating formal specifications using FCA. This architecture is realised using ZML and ToscanaJ to produce a practical research tool. The thesis also includes the first broad survey of FCA in the domain of software engineering and an FCA-based methodology for surveying academic literature in general.

Currently, the bulk of applications of Formal Concept Analysis (FCA) in software engineering have focussed on software maintenance and re-engineering. In this thesis we broaden the approach by applying FCA to a number of early-phase activities within the software engineering life-cycle. With respect to the requirements engineering phase, a case study is presented comparing two class hierarchies that model aspects of a mass-transit railway ticketing system. The first hierarchy was produced for an existing Object-Z specification of the system while the second was derived using FCA. Contrasting the two hierarchies revealed that they were essentially the same, however, the differences highlighted specification artefacts in the existing hierarchy. With respect to the design phase, the thesis discusses the use of FCA for the navigation and visualisation of Formal Specifications written in Z. In response to the continued call for formal methods tool support, we implement and explore a prototype specification browser that exploits the abstractions afforded by FCA. The research hypothesis is an integrated architecture for navigating formal specifications using FCA. This architecture is realised using ZML and ToscanaJ to produce a practical research tool. The thesis also includes the first broad survey of FCA in the domain of software engineering and an FCA-based methodology for surveying academic literature in general.