Evaluation of agri-environmental and forestry schemes with multiple objectives

The evaluation of EU policy in the area of rural land use management often encounters problems of multiple and poorly articulated objectives. Agri-environmental policy has a range of aims, including natural resource protection, biodiversity conservation and the protection and enhancement of landscape quality. Forestry policy, in addition to production and environmental objectives, increasingly has social aims, including enhancement of human health and wellbeing, lifelong learning, and the cultural and amenity value of the landscape. Many of these aims are intangible, making them hard to define and quantify. This article describes two approaches for dealing with such situations, both of which rely on substantial participation by stakeholders. The first is the Agri-Environment Footprint Index, a form of multi-criteria participatory approach. The other, applied here to forestry, has been the development of ‘multi-purpose’ approaches to evaluation, which respond to the diverse needs of stakeholders through the use of mixed methods and a broad suite of indicators, selected through a participatory process. Each makes use of case studies and involves stakeholders in the evaluation process, thereby enhancing their commitment to the programmes and increasing their sustainability. Both also demonstrate more ‘holistic’ approaches to evaluation than the formal methods prescribed in the EU Common Monitoring and Evaluation Framework.

Analyzing security protocols using association rule mining

Current studies to analyzing security protocols using formal methods require users to predefine authentication goals. Besides, they are unable to discover potential correlations between secure messages. This research attempts to analyze security protocols using data mining. This is done by extending the idea of association rule mining and converting the verification of protocols into computing the frequency and confidence of inconsistent secure messages. It provides a novel and efficient way to analyze security protocols and find out potential correlations between secure messages. The conducted experiments demonstrate our approaches.

Normative-informational positions: a modal-logical approach

This paper is a preliminary investigation into the application of the formal-logical theory of normative positions to the characterisation of normative-informational positions, pertaining to rules that are meant to regulate the supply of information. First, we present the proposed framework. Next, we identify the kinds of nuances and distinctions that can be articulated in such a logical framework. Finally, we show how such nuances can arise in specific regulations. Reference is made to Data Protection Law and Contract Law, among others. The proposed approach is articulated around two essential steps. The first involves identifying the set of possible interpretations that can be given to a particular norm. This is done by using formal methods. The second involves picking out one of these interpretations as the most likely one. This second step can be resolved only by using further information (e.g., the context or other parts of the regulation).

Probabilistic reasoning of inconsistent belief in protocol analysis

Security protocols have been recently found with subtle flaws due to incomplete or ambiguous specification. Although formal methods have remarkably assisted in protocol analysis, they ignores the effect of hostile/uncertain environment, which might lead to inconsistent belief that can be held by principals in delivered messages. This discrepant belief may prevent us from representing the insecurity and uncertainty in a real trading situation. Unfortunately, the current approaches lack the ability to handle the inconsistent belief. This article presents a probabilistic method, which intuitively measures the belief from different principals that can be put on the goal of the protocol. The experiments demonstrate our method is useful to enhance the protocol analysis.

Managing design knowledge with mixed-initiative dialogue

This paper is based on ongoing work in developing interactive interfaces to formal methods for encoding design knowledge. It reports on the development of a shared graphical notation to support user interaction with design knowledge based on mixed-initiative. Mixed-initiative provides a model of interaction where both the designer and the knowledge formalism may share responsibility over decisions. The paper discusses how a formal visual notation can support the mixed-initiative mode for developing and managing formal design knowledge. The notation addresses on the dialogue problem between the user and a knowledge based formalism and illustrates a model of interaction in which the user and the formalism can share and input data through a common shared resource, on a common shared task. The paper demonstrates the use of this notation in common decision tasks and the implications for seamless interaction with design support systems.

Rule-based dependency models for security protocol analysis

Security protocol analysis has been discussed for quite some time in the past few years. Although formal methods have been widely used to identify various vulnerabilities, mainly susceptibility to freshness attacks and impersonation, the arisen inconsistent data between principals and collusion attacks held by a group of dishonest principals have been largely ignored. Moreover, the previous methods focus on reasoning about certain security-related properties and detecting known attacks against secure message, whereas there have been insufficient efforts to handle the above hidden but powerful attacks. In this paper, we address these critical issues and prove the efficiency and intuitiveness of rule-based dependency models in defending a protocol against the attacks. This is able to provide a numerical estimation to measure he occurrence of these attacks. It will be useful in enhancing the current protocol analysis.

Agents based e-commerce and securing exchanged information

Mobile agents have been implemented in e-commerce to search and filter information of interest from electronic markets. When the in format ion is very sensitive and critical, it is important to develop a novel security protocol that can efficiently protect the information from malicious tampering as well as unauthorized disclosure or at least detect any malicious act of intruders. In this chapter, we describe robust security techniques that ensure a sound security of information gathered throughout agent's itinerary against various security attacks, as well as truncation attacks. A sound security protocol is described , which implements the various security techniques that would jointly prevent or at least detect any malicious act of intruders. We reason about the soundness of the protocol using Symbolic Trace Analyzer (STA), a formal verification tool that is based on symbolic techniques. We analyze the protocol in key configurations and show that it is free of flaws. We also show that the protocol fulfils the various security requirements of exchanged information in MAS, including data-integrity, data-confidentiality, data authenticity, origin confidentiality and data non-repudiability.

Forensic identification of students outsourcing assignment projects from freelancer.com

This paper reports the increasing popularity of outsourcing academic works by university students motivated by the lure of lucrative dividends and visa opportunities. Due to a lack of formal methods in detecting such transactions, freelance websites are thriving in facilitating the trade of outsourced assignments. This is compounded by the fact that many university staff have neither the time nor training to perform complex media analysis and forensic investigations. This paper proposes a method to aid in the identification of those who outsource assignment works on the most popular site freelancer.com. We include a recent real-world case study to demonstrate the relevancy and applicability of our methodology. In this case study, a suspect attempts to evade detection via use of anti-forensics which demonstrates the capability and awareness of evasion techniques used by students.

JCML - Java Card Modeling Language: Definição e Implementação

Formal methods should be used to specify and verify on-card software in Java Card applications. Furthermore, Java Card programming style requires runtime verification of all input conditions for all on-card methods, where the main goal is to preserve the data in the card. Design by contract, and in particular, the JML language, are an option for this kind of development and verification, as runtime verification is part of the Design by contract method implemented by JML. However, JML and its currently available tools for runtime verification were not designed with Java Card limitations in mind and are not Java Card compliant. In this thesis, we analyze how much of this situation is really intrinsic of Java Card limitations and how much is just a matter of a complete re-design of JML and its tools. We propose the requirements for a new language which is Java Card compliant and indicate the lines on which a compiler for this language should be built. JCML strips from JML non-Java Card aspects such as concurrency and unsupported types. This would not be enough, however, without a great effort in optimization of the verification code generated by its compiler, as this verification code must run on the card. The JCML compiler, although being much more restricted than the one for JML, is able to generate Java Card compliant verification code for some lightweight specifications. As conclusion, we present a Java Card compliant variant of JML, JCML (Java Card Modeling Language), with a preliminary version of its compiler

Deciding difference logic in a Nelson-Oppen combination framework

O método de combinação de Nelson-Oppen permite que vários procedimentos de decisão, cada um projetado para uma teoria específica, possam ser combinados para inferir sobre teorias mais abrangentes, através do princípio de propagação de igualdades. Provadores de teorema baseados neste modelo são beneficiados por sua característica modular e podem evoluir mais facilmente, incrementalmente. Difference logic é uma subteoria da aritmética linear. Ela é formada por constraints do tipo x − y ≤ c, onde x e y são variáveis e c é uma constante. Difference logic é muito comum em vários problemas, como circuitos digitais, agendamento, sistemas temporais, etc. e se apresenta predominante em vários outros casos. Difference logic ainda se caracteriza por ser modelada usando teoria dos grafos. Isto permite que vários algoritmos eficientes e conhecidos da teoria de grafos possam ser utilizados. Um procedimento de decisão para difference logic é capaz de induzir sobre milhares de constraints. Um procedimento de decisão para a teoria de difference logic tem como objetivo principal informar se um conjunto de constraints de difference logic é satisfatível (as variáveis podem assumir valores que tornam o conjunto consistente) ou não. Além disso, para funcionar em um modelo de combinação baseado em Nelson-Oppen, o procedimento de decisão precisa ter outras funcionalidades, como geração de igualdade de variáveis, prova de inconsistência, premissas, etc. Este trabalho apresenta um procedimento de decisão para a teoria de difference logic dentro de uma arquitetura baseada no método de combinação de Nelson-Oppen. O trabalho foi realizado integrando-se ao provador haRVey, de onde foi possível observar o seu funcionamento. Detalhes de implementação e testes experimentais são relatados

Joker: um realizador de desenhos animados para linguagens formais

Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the system s properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++.

Estendendo CRefine para o suporte de táticas de refinamento

The use of increasingly complex software applications is demanding greater investment in the development of such systems to ensure applications with better quality. Therefore, new techniques are being used in Software Engineering, thus making the development process more effective. Among these new approaches, we highlight Formal Methods, which use formal languages that are strongly based on mathematics and have a well-defined semantics and syntax. One of these languages is Circus, which can be used to model concurrent systems. It was developed from the union of concepts from two other specification languages: Z, which specifies systems with complex data, and CSP, which is normally used to model concurrent systems. Circus has an associated refinement calculus, which can be used to develop software in a precise and stepwise fashion. Each step is justified by the application of a refinement law (possibly with the discharge of proof obligations). Sometimes, the same laws can be applied in the same manner in different developments or even in different parts of a single development. A strategy to optimize this calculus is to formalise these application as a refinement tactic, which can then be used as a single transformation rule. CRefine was developed to support the Circus refinement calculus. However, before the work presented here, it did not provide support for refinement tactics. The aim of this work is to provide tool support for refinement tactics. For that, we develop a new module in CRefine, which automates the process of defining and applying refinement tactics that are formalised in the tactic language ArcAngelC. Finally, we validate the extension by applying the new module in a case study, which used the refinement tactics in a refinement strategy for verification of SPARK Ada implementations of control systems. In this work, we apply our module in the first two phases of this strategy