| 1 |
SawjaCard: A Static Analysis Tool for Certifying Java Card Applications
|
|
|
|
In: 21st International Static Analysis Symposium (SAS 2014) ; https://hal.inria.fr/hal-01093327 ; 21st International Static Analysis Symposium (SAS 2014), 2014, Munich, Germany. pp.51 - 67, ⟨10.1007/978-3-319-10936-7_4⟩ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 2 |
A Precise and Abstract Memory Model for C Using Symbolic Values
|
|
|
|
In: 12th Asian Symposium on Programming Languages and Systems (APLAS 2014) ; https://hal.inria.fr/hal-01093312 ; 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. pp.449 - 468, ⟨10.1007/978-3-319-12736-1_24⟩ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 3 |
Planning Human-Computer Improvisation
|
|
|
|
In: International Computer Music Conference ; https://hal.archives-ouvertes.fr/hal-01053834 ; International Computer Music Conference, Sep 2014, Athens, Greece ; http://icmc14-smc14.net (2014)
|
|
BASE
|
|
Show details
|
|
|
| 4 |
The Package Blueprint: visually analyzing and quantifying package dependencies
|
|
|
|
In: ISSN: 0167-6423 ; Science of Computer Programming ; https://hal.inria.fr/hal-00957695 ; Science of Computer Programming, Elsevier, 2014, 89 (Part C), pp. 298-319. ⟨10.1016/j.scico.2014.02.016⟩ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 5 |
ЯЗЫК СПЕЦИФИКАЦИИ ВИРТУАЛЬНОГО ОБОРУДОВАНИЯ ЭМУЛЯТОРОВ ЭВМ
|
|
БУРЛАКОВ АЛЕКСЕЙ СЕРГЕЕВИЧ. - : Федеральное государственное бюджетное образовательное учреждение высшего образования «Иркутский национальный исследовательский технический университет», 2014
|
|
BASE
|
|
Show details
|
|
|
| 6 |
COSMO : a Bayesian model of sensori-motor interactions in speech perception ; COSMO : un modèle bayésien des interactions sensori-motrices dans la perception de la parole
|
|
|
|
In: https://tel.archives-ouvertes.fr/tel-01113286 ; Autre [cs.OH]. Université de Grenoble, 2014. Français. ⟨NNT : 2014GRENM063⟩ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 7 |
Logically timed specifications in the AADL : a synchronous model of computation and communication (recommendations to the SAE committee on AADL)
|
|
|
|
In: https://hal.inria.fr/hal-00970244 ; [Technical Report] RT-0446, INRIA. 2014, pp.27 (2014)
|
|
Abstract:
The purpose of this document is to provide an analysis of the SAE standard AADL (AS5506) and submit recommendations for equipping it with a synchronous model of computation and communication (MoCC). Our goal is to provide a framework that best fits the semantic and expressive capability of the AADL, and is designed in a way that requires as few conceptual, semantic, or syntactic extensions as possible, on either the standard or its existing annexes. Our approach consists of the definition of an algebraic framework in which time is formally defined from implicit or specified AADL concepts, such as events. Starting from these concepts, that constitute the synchronous core of the AADL, we define a formal design methodology to use the AADL in a way that supports formal analysis, verification and synthesis of timed properties. By putting forward synchrony and timing, we intend to define time starting from software and hardware events that incur synchronisation in an architecture specification. Synchronisation indeed is the fundamental artefact from which time can be sensed, in either software or hardware. Synchrony relates to that fundamental concept as a model of computation and communication, applicable to both software and hardware design. It puts emphasis on logical time, abstracted through synchronisation points, in order to break down computations into zero-time reactions and regard communications as instantaneous. While abstracting real time, synchronous logical time provides an algebraic framework in which both event-driven and time-triggered execution policies can be specified. Bridging the gap between system-level, logical, synchronous specifications and time-triggered, distributed, and dynamically scheduled real-time applications necessitates a refinement-based design methodology, which we additionally intend to outline, to support the applicability of the proposed concepts in system design. To support the formal presentation of our MoCC, we define a algebra of automata consisting of transition systems and logical timing constraints. We consider the behaviour annex (BA) as the mean to implement this model, together with the constraint annex (CA), as a mean to represent abstractions of behaviour annexes using clock constraints and regular expressions. ; L'architecture logiciel d'un système embarqué est un artefact de conception de constituants hétérogènes au croisement de plusieurs points de vue: logiciel, matériel, physique. Le temps à une nature différente quand il est observé de ces points de vue différents : il est discret et évènementiel vu du logiciel, discret et périodique vu du matériel, et continu en physique. Il n'est pas surprenant que ce soit une notion commune à l'architecte d'un système, étant donné sa criticité, sa diversité, la difficulté de le maitriser. Pour compliquer les choses un peu plus, les formalismes de spécification et de programmation de haut-niveau utilisés pour spécifier ces systèmes altèrent significativement cette perception du temps. Dans un modèle physique, on simule le temps par des équations différentielles dont la résolution est discrète. Dans un modèle matériel, on représente les circuits par différents niveaux d'abstractions pour faire face à leur complexité: registre, transaction, système. Dans un modèle logiciel, on abstrait le temps par un modèle conceptuel de la concurrence, pas exemple synchrone. Délivrer un cadre mathématique, des outils de vérification et de synthèse, pour analyser, composer, orchestrer ces modèles serait d'une valeur inestimable pour l'architecte d'un système. L'architecte travaille en effet d'un point de vue ou' toutes les composantes d'un système: logiciel, intergiciel, matériel, environnement; doivent être analysés, profilés, évalués, composés, simulés et validés. L'objectif de ce document est de proposer un cadre méthodologique formel pour conduire le travail de l'architecte: l'exploration d'architecture et le prototypage virtuel de systèmes embarqués. Pour définir cette méthodologies, nous nous appuyons sur le standard AADL (architecture analysis description language) du consortium SAE, auquel nous recommandons la définition d'une annexe temporelle au standard.
|
|
Keyword:
!formal!semantics!and!analysis; !SAE!standard!AADL!; !synchronous!programming; [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]; [INFO.INFO-ES]Computer Science [cs]/Embedded Systems; [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation; [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH]; [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]; ACM: D.: Software/D.2: SOFTWARE ENGINEERING; ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.1: Requirements/Specifications; ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.2: Design Tools and Techniques; ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification; ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory; ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.3: Language Constructs and Features; ACM: I.: Computing Methodologies; embedded!system!design
|
|
URL: https://hal.inria.fr/hal-00970244v2/file/RT_446.pdf
https://hal.inria.fr/hal-00970244
https://hal.inria.fr/hal-00970244v2/document
|
|
BASE
|
|
Hide details
|
|
|
| 8 |
Polymorphic Functions with Set-Theoretic Types. Part 1: Syntax, Semantics, and Evaluation
|
|
|
|
In: POPL '14, 41th ACM Symposium on Principles of Programming Languages ; https://hal.archives-ouvertes.fr/hal-00907166 ; POPL '14, 41th ACM Symposium on Principles of Programming Languages, Jan 2014, San Diego, United States. pp.5-17, ⟨10.1145/2535838.2535840⟩ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 9 |
Code Your Own Game: The Case of Children with Hearing Impairments
|
|
|
|
In: Lecture Notes in Computer Science ; 13th International Conference Entertainment Computing (ICEC) ; https://hal.inria.fr/hal-01408511 ; 13th International Conference Entertainment Computing (ICEC), Oct 2014, Sydney, Australia. pp.108-116, ⟨10.1007/978-3-662-45212-7_14⟩ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 10 |
Dislog: a Logic-Based Language for Processing Discourse
|
|
|
|
In: Logic Programming: Theory, Practices and Challenges - Proceedings of the 8th International Conference on Language Resources and Evaluation (LREC 2012) ; https://hal.archives-ouvertes.fr/hal-03224122 ; Columbus, Nadya. Logic Programming: Theory, Practices and Challenges - Proceedings of the 8th International Conference on Language Resources and Evaluation (LREC 2012), L12-1 (paper 17), European Language Resources Association (ELRA), pp.2770-2777, 2014 ; https://www.aclweb.org/anthology/L12-1017/ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 11 |
Automating Variability Model Inference for Component-Based Language Implementations
|
|
|
|
In: SPLC'14 - 18th International Software Product Line Conference ; https://hal.inria.fr/hal-01023864 ; SPLC'14 - 18th International Software Product Line Conference, Sep 2014, Florence, Italy (2014)
|
|
BASE
|
|
Show details
|
|
|
| 12 |
τC: C with process network extensions for embedded manycores
|
|
|
|
In: ISSN: 1877-0509 ; EISSN: 1877-0509 ; Procedia Computer Science ; https://hal-cea.archives-ouvertes.fr/cea-01831559 ; Procedia Computer Science, Elsevier, 2014, 29, pp.1100-1112. ⟨10.1016/j.procs.2014.05.099⟩ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 13 |
Instrumentation of annotated c programs for test generation
|
|
|
|
In: 2014 IEEE 14th International Working Conference on Source Code Analysis and Manipulation ; https://hal-cea.archives-ouvertes.fr/cea-01836306 ; 2014 IEEE 14th International Working Conference on Source Code Analysis and Manipulation, Sep 2014, Victoria, Canada. pp.105-114, ⟨10.1109/SCAM.2014.19⟩ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 14 |
Mezzo: a typed language for safe effectful concurrent programs ; Mezzo: un langage typé pour programmer de manière concurrent et sure en présence d'effets
|
|
|
|
In: https://hal.inria.fr/tel-01086106 ; Programming Languages [cs.PL]. Université Paris Diderot - Paris 7, 2014. English (2014)
|
|
BASE
|
|
Show details
|
|
|
| 15 |
Mining Relevant Sequence Patterns with CP-based Framework
|
|
|
|
In: IEEE Int. Conf. on Tools with Artificial Intelligence (ICTAI 2014) ; https://hal.archives-ouvertes.fr/hal-01145905 ; IEEE Int. Conf. on Tools with Artificial Intelligence (ICTAI 2014), 2014, Limassol,, Cyprus. pp.552-559 (2014)
|
|
BASE
|
|
Show details
|
|
|
| 17 |
Description and Optimization of Abstract Machines in a Dialect of Prolog ...
|
|
|
|
BASE
|
|
Show details
|
|
|
| 18 |
BACIBeans: A NetBeans Plugin for Concurrent Programs
|
|
|
|
In: Seaver College Research And Scholarly Achievement Symposium (2014)
|
|
BASE
|
|
Show details
|
|
|
| 19 |
A Language Support for Exhaustive Fault-Injection in Message-Passing System Models ...
|
|
|
|
BASE
|
|
Show details
|
|
|
|
|
