1,721,482 research outputs found
Development of a System Controlling Cars on a Bridge using Machine Inclusion
No full textThis dataset is associated with the following paper: Thai Son Hoang, Dana Dghaym, Colin Snook, and Michael Butler. A Composition Mechanism for Refinement-Based Methods. In Zhenjiang Hu and Guangdong Bai, editors, *ICECCS'17: International Conference on Engineering of Complex Computer Systems, Fukuoka, Japan, November 5--8, Proceedings*, IEEE, 2017. Details about the dataset can be found in the README.md file.</span
Dang Thai Son, piano (Vietnam)
No full textConcierto interpretado por Dang Thai Son. El pianista vietnamita llamó la atención del mundo musical al ganar la Medalla de Oro y otros premios especiales en el XII Concurso Internacional Chopin (Varsovia, octubre de 1980). Por primera vez un pianista asiático obtenía las más altas distinciones en el que, para muchos, es el más importante concurso de piano, su carrera internacional le ha llevado contínuamente a más de 30 países. Es regularmente invitado por las orquestas filarmónicas de Dresde, Leningrado, Oslo, Varsovia, Helsinki, Moscú, de la BBC, por las sinfónicas de Praga, Montreal, Berlín, Hungría, Sidney. de la NHK, y por las más importantes orquestas de cámara europeas.
En este concierto interpreto obras de Franz Schubert, Claude Debussy y Frederic Chopin
Towards generating SPARK from Event-B models
No full textThis paper presents an approach to generate SPARK code from Event-B models. System models in Event-B are translated into SPARK packages including proof annotations. Properties of the Event-B models such as axioms and invariants are also translated and embedded in the resulting models as pre- and post-conditions. This helps with generating SPARK proof annotations automatically hence ensuring the correct behaviour of the resulting code. A prototype plug-in for the Rodin has been developed and the approach is evaluated on different examples. We also discuss the possible extensions including to generate scheduled code and data structures such as records
Decomposition tool for Event-B
No full textTwo methods have been identified for Event-B model decomposition: shared variable and shared event. The purpose of this paper is to introduce the two approaches and the respective tool support in the Rodin platform. Besides alleviating the complexity for large systems and respective proofs, decomposition allows team development in parallel over the same model which is very attractive in the industrial environment
Dataset for "An STPA-based formal composition framework for trustworthy autonomous maritime systems"
No full textThe data set contains the following material
- *imms_classdiagram.zip* and *imms_statemachine.zip*: System model using UML-B class diagrams and statemachine
- *MP2.zip*: Archive of the model for communication link MP2 in Event-B/Rodin
</span
Dataset for "Towards Generating SPARK from Event-B Models"
No full textDataset supports: Sritharan, S & Hoang, TS 2020, Generating SPARK from Event-B Models. in Proceedings of the 16th International Conference on integrated Formal Methods. The 16th International Conference on integrated Formal Methods, Lugano, Switzerland, 16/11/20.</span
Rodin Developments for Formal Policing Functions based on Metamorphic Relations
No full textThe Rodin archives of the developments are as follows
- PFGeneric.zip: Generic policing function based on metamorphic testings
- ShortestPath.zip: Policing function for traffic sign image recognition
- TrafficSigns.zip: Policing function for finding shortest paths program</span
The hybrid ERTMS/ETCS level 3 case study
No full textThis document presents a description of the European Rail Traffic Management System (ERTMS) case study. ERTMS is a system of standards for management and interoperation of signalling for railways by the European Union (EU). The case study focuses on the ERTMS Level 3 Hybrid principle, which accommodates different types of trains including ERTMS trains equiped with the Train Integrity Monitoring System (TIMS), ERTMS trains without TIMS, and non-ERTMS trains.</p
iUML-B model of VLAN system
No full textDataset support the paper 'Analysing security protocols using refinement in iUML-B', presented at 9th NASA Formal Methods Symposium, 16-18 May 2017.
Formal specification of a VLAN tagging system illustrating the well-known security flaw of these systems, double-tagging. We use iUML-B class diagrams which provide a diagrammatic representation of the Event-B formalism. We specify the security principle that packets should only belong to nodes of a VLAN which they are intended for and prove that the property is maintained. We then refine the model to introduce the usual packet tagging mechanism that is supposed to ensure the security principle. A double tagging attack cannot be proven to satisfy the glueing invariant. A second version of the model is provided that excludes the Native LAN from being used as a VLAN which is the usual recommendation to prevent double-tagging attacks. This version is fully proven to be secure.</span
Rodin Prototype Plug-ins and Development of the SecBot Case Study
No full textDataset supporting "Refinement of Statecharts with Run-to-Completion Semantics"
Presented at FTSCS 2018 - The 6th International Workshop on Formal Techniques for Safety-Critical Systems, 16th November 2018, Gold Coast, Australia</span
- …
