Búsqueda avanzada

El autor Clara Benac Earle ha publicado 5 artículo(s):

1 - Automatic Grading of Programming Exercises using Property-Based Testing

We present a framework for automatic grading of programming exercises using property-based testing, a form of model-based black-box testing. Models are developed to assess both the functional behaviour of programs and their algorithmic complexity. From the functional correctness model a
large number of test cases are derived automatically. Executing them on the body of exercises gives rise to a (partial) ranking of programs, so that a program A is ranked higher than program B if it fails a strict subset of the test cases failed by B. The model for algorithmic complexity is used to compute worst-case complexity bounds. The framework moreover considers code structural metrics, such as McCabe’s cyclomatic complexity, giving rise to a composite program grade that includes both functional, non-functional, and code structural aspects. The framework is evaluated in a course teaching algorithms and data structures using Java.

Autores: Clara Benac Earle  / Lars-Ake Fredlund / John Hughes / 
Palabras Clave:

2 - Evaluación de Requisitos de Seguridad con MBASafe conforme a la norma EN 50128 (Trabajo de alto nivel)

According to EN 50129, manufacturers of rail vehicles shall justify via a safety case that their vehicles are adequately safe for their intended applications. MBASafe is a recently proposed and potentially innovative design and verification process. In the presence of compelling arguments concerning its adequacy as process evidence, MBASafe could support the safety claims within the required safety cases.
In this paper, we contribute to partially justify the adequacy of MBASafe to act as process evidence. To do that, we first manually check if MBASafe includes EN 50128-compliant process elements, then we model MBASafe in compliance with Software Process Engineering Meta-model 2.0, then, we derive process-based arguments from the MBASafe process model by using MDSafeCer, the recently introduced Model Driven Safety Certification method. By doing so, we provide a twofold contribution: we further validate MDSafeCer in the rail domain and we strengthen MBASafe.

Autores: Barbara Gallina / Elena Gómez-Martínez / Clara Benac Earle / 
Palabras Clave: EN 5012x - model-driven safety certication - process assessment

3 - Pitfalls of Jason Concurrency

Jason is a well-known programming language for multia-gent systems where fine-grained concurrency primitives allow a highly-concurrent efficient execution. However, typical concurrency errors suchas race conditions are hard to avoid. In this chapter, we analyze a numberof such potential pitfalls of the Jason concurrency model, and, describeboth how such risks can be mitigated in Jason itself, as well as discussingthe alternatives implemented in eJason, an experimental extension of Ja-son with support for distribution and fault tolerance. In some cases, wepropose changes in the standard Jason semantics.

Autores: Álvaro Fernández Díaz / Clara Benac Earle / Lars-Ake Fredlund / 
Palabras Clave: BDI - Concurrency - Jason programming

4 - Gaining Trust by Tracing Security Protocols

In this article we test an Erlang implementation of the NoiseProtocol Framework, using a novel form of white-box testing.We extend interoperability testing of an Erlang enoise imple-mentation against an implementation of Noise in C. Testingtypically performs a noise protocol handshake between thetwo implementations. If successful, then both implementa-tions are somehow compatible. But this does, for example,not detect whether we reuse keys that have to be newly gen-erated. Therefore we extend such operability testing: Duringthe handshake the Erlang noise implementation is traced.The resulting protocol trace is refactored, obtaining as theend result a symbolic description (a functional term) of howkey protocol values are constructed using cryptographic op-erations and keys. Therafter, this symbolic term is compared,using term rewriting, with a symbolic term representing theideal symbolic execution of the tested noise protocol hand-shake (i.e., the “semantics” of the handshake). The semanticsymbolic term is obtained by executing a symbolic imple-mentation of the noise protocol that we have developed.

Autores: Lars-Ake Fredlund / Clara Benac Earle / Thomas Arts / Hans Svensson / 
Palabras Clave: Erlang - Noise - Original publication in the 2019 ACM SIGPLAN Erlang Workshop. - Security Protocols - Tracing

5 - A Formal Semantics for Agent Distribution and Fault Tolerance in Jason

This paper provides a formal specification of the distribution and fault-tolerancemechanisms of eJason. The eJason programming language is an extension tothe agent-oriented programming language Jason that introduces native supportfor the transparent distribution of agents as well as fault-tolerance mechanisms.This formal semantics is presented from a multiagent system perspective. Itunambiguously describes both the possible evolution of the distributed multi-agent system over time and the different instruments for fault detection andfault recovery, hence exposing their strengths. This specification may serve asa reference for researchers interested in the inclusion of similar mechanisms inagent-oriented programming languages.

Autores: Álvaro Fernández Díaz / Lars-Ake Fredlund / Clara Benac Earle / Julio Mariño / 
Palabras Clave: Erlang - Formal semantics - Multiagent systems