Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Using Assurance Cases and Boolean Logic Driven Markov Processes to Formalise Cyber Security Concerns for Safety-Critical Interaction with Global Navigation Satellite Systems
Get PDFSatellite-based location and timing systems support a wide range of mass market applications, typically using the GPS infrastructure. Until recently, these applications could not be used within safety-critical interfaces. Limits to the accuracy, availability, integrity and continuity of the space-based signals prevented regulatory agencies from certifying their use. Over the last three months, however, the latest generation of augmented Global Navigation Satellite Systems (GNSS) have been approved for use in safety-related applications. They use a range of techniques to overcome the limitations of previous infrastructures. This means that they can be used as primary navigation tools in a wide range of interactive systems, including aircraft cockpits, railway signalling tools etc. Unfortunately, a range of organisations including the UK Ministry of Defence, have raised concerns about our increasing vulnerability to attacks on these satellite based architectures. These threats are compounded by the difficulty of representing and reasoning about the impact of jamming, spoofing and insider threats for the end-users of safety-critical systems. A sudden loss of navigational support can undermine users confidence in complex applications and pose a significant threat to distributed situation awareness. We show how formal reasoning techniques can be used to identify the safety and security concerns that jeopardise interaction with future generations of Global Navigation Satellite Systems applications
Self Organized Swarms for cluster preserving Projections of high-dimensional Data
Get PDFA new approach for topographic mapping, called Swarm-Organized Projection (SOP) is presented. SOP has been inspired by swarm intelligence methods for clustering and is similar to Curvilinear Component Analysis (CCA) and SOM. In contrast to the latter the choice of critical parameters is substituted by self-organization. On several crucial benchmark data sets it is demonstrated that SOP outperforms many other projection methods. SOP produces coherent clusters even for complex entangled high dimensional cluster structures. For a nontrivial dataset on protein DNA sequence Multi Dimensional Scaling (MDS) and CCA fail to represent the clusters in the data, although the clusters are clearly defined. With SOP the correct clusters in the data could be easily detected
Mobile CSP||B
Get PDFCSP||B is a combination of CSP and B in which
CSP processes are used as control executives for B machines. This architecture enables a B machine and its controller to interact and communicate with each
other while working in parallel. The architecture has focused on sequential CSP processes as dedicated controllers for B machines. This paper introduces Mobile CSP||B, a formal framework based on CSP||B which enables us to specify and verify concurrent systems with mobile architecture
instead of the previous static architecture. In Mobile CSP||B,
a parallel combination of CSP processes act as the control executive for the B machines and these B machines can be transferred between CSP processes during the system execution. The paper introduces the foundations of the
approach, and illustrates the result with an example
Damages and Benefits of Certification: A perspective from an Independent Assessment Body
Get PDFThe paper investigates on the nature of software certification and its reasons of being. The numerous factors that impact on the achievement of its purposes are discussed, and also compared in the cases of Proprietary Software and Open Source Software. Some relevant features of a certification process for Open Source Software are finally proposed
UI-Design Driven Model-Based Testing
Get PDFTesting interactive systems is notoriously difficult. Not only do we need to ensure that the functionality of the developed system is correct with respect to the requirements and specifications, we also need to ensure that the user interface to the system is correct (enables a user to access the functionality correctly) and is usable. These different requirements of interactive system testing are not easily combined within a single testing strategy. We investigate the use of models of interactive systems, which have been derived from design artefacts, as the basis for generating tests for an implemented system. We give a model-based method for testing interactive systems which has low overhead in terms of the models required and which enables testing of UI and system functionality from the perspective of user interaction
Towards a Conceptual Framework Supporting Model Compilability
Get PDFThe ever-growing use of modeling languages today is largely due to a maturation of model-based development technologies. However, there is enough room for improving language specifications and consequently, the efficiency of their usage. The state of facts in specifying Well Formedness Rules is among the most important issues calling for improvements. Despite the fact that various papers have approached it, the topic is still open. To solve it, there is the need of a rigorous conceptual framework supporting the specification of modeling languages’ static semantics. This would stand as a basis for ensuring model compilability, a mandatory requirement in a model-driven context. Through this paper, we aim at providing core ideas that would contribute to the creation of such a framework. Our approach is testing-oriented and promotes the use of OCL specification patterns
GUI Inspection from Source Code Analysis
Get PDFGraphical user interfaces (GUIs) are critical components of todays software. Given their increased relevance, correctness and usability of GUIs are becoming essential. This paper describes the latest results in the development of our tool to reverse engineer the GUI layer of interactive computing systems. We use static analysis techniques to generate models of the user interface behaviour from source code. Models help in graphical user interface inspection by allowing designers to concentrate on its more important aspects. One particular type of model that the tool is able to generate is state machines. The paper shows how graph theory can be useful when applied to these models. A number of metrics and algorithms are used in the analysis of aspects of the user interface’s quality. The ultimate goal of the tool is to enable analysis of interactive system through GUIs source code inspection
Co-tabulations, Bicolimits and Van-Kampen Squares in Collagories
Get PDFWe previously defined collagories essentially as “distributive allegories without zero morphisms”. Collagories are sufficient for accommodating the relation-algebraic approach to graph transformation, and closely correspond to the adhesive categories important for the categorical DPO approach to graph transformation.
Heindel and Sobocinski have recently characterised the Van-Kampen colimits used in adhesive categories as bicolimits in span categories.
In this paper, we study both bicolimits and lax colimits in collagories. We show that the relation-algebraic co-tabulation concept is equivalent to lax colimits of difunctional morphisms and to bipushouts, but much more concise and accessible. From this, we also obtain an interesting characterisation of Van-Kampen squares in collagories
