Imperial College London
Professor Nobuko Yoshida

ProfessorNobukoYoshida

Faculty of Engineering, Department of Computing

Academic Visitor
 
 
 
//

Contact

 

+44 (0)20 7594 8240n.yoshida Website

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

373 results found

Bocchi L, Chen T-C, Demangeon R, Honda K, Yoshida Net al., 2013, Monitoring networks through multiparty session types, Departmental Technical Report: 13/3, Publisher: Department of Computing, Imperial College London, 13/3

In large-scale distributed infrastructures, applications are realisedthrough communications among distributed components. The needfor methods for assuring safe interactions in such environments is recognized,however the existing frameworks, relying on centralised veri cationor restricted speci cation methods, have limited applicability. This paperproposes a new theory of monitored -calculus with dynamic usage ofmultiparty session types (MPST), o ering a rigorous foundation for safetyassurance of distributed components which asynchronously communicatethrough multiparty sessions. Our theory establishes a framework for semanticallyprecise decentralised run-time enforcement and provides reasoningprinciples over monitored distributed applications, which complementexisting static analysis techniques. We introduce asynchronythrough the means of explicit routers and global queues, and proposenovel equivalences between networks, that capture the notion of interfaceequivalence, i.e. equating networks o ering the same services to a user.We illustrate our static-dynamic analysis system with an ATM protocolas a running example and justify our theory with results: satisfactionequivalence, local/global safety and transparency, and session delity.

Report

Honda K, Yoshida N, Berger M, 2013, An observationally complete program logic for imperative higher-order functions, Departmental Technical Report: 13/2, Publisher: Department of Computing, Imperial College London, 13/2

We propose a simple compositional program logic for an imperative extensionof call-by-value PCF, built on Hoare logic and our preceding work on program logics forpure higher-order functions. A systematic use of names and operations on them allowsprecise and general description of complex higher-order imperative behaviour. The proofrules of the logic exactly follow the syntax of the language and can cleanly embed, justifyand extend the standard proof rules for total correctness of Hoare logic. The logicoffers a foundation for general treatment of aliasing and local state on its basis, withminimal extensions. After establishing soundness, we prove that valid assertions for programscompletely characterise their behaviour up to observational congruence, which isproved using a variant of finite canonical forms. The use of the logic is illustrated throughreasoning examples which are hard to assert and infer using existing program logics.

Report

Denielou P-M, Yoshida N, 2013, Multiparty compatibility in communicating automata: characterisation and synthesis of global session types, Departmental Technical Report: 13/5, Publisher: Department of Computing, Imperial College London, 13/5

Multiparty session types are a type system that can ensure the safetyand liveness of distributed peers via the global specification of their interactions.To construct a global specification from a set of distributed uncontrolledbehaviours, this paper explores the problem of fully characterising multipartysession types in terms of communicating automata. We equip global and localsession types with labelled transition systems (LTSs) that faithfully representasynchronous communications through unbounded buffered channels. Using theequivalence between the two LTSs, we identify a class of communicating automatathat exactly correspond to the projected local types. We exhibit an algorithmto synthesise a global type from a collection of communicating automata.The key property of our findings is the notion of multiparty compatibility whichnon-trivially extends the duality condition for binary session types.

Report

Kouzapas D, Yoshida N, 2013, Globally governed session semantics, Departmental Technical Report: 13/4, Publisher: Department of Computing, Imperial College London, 13/4

This paper proposes a new bisimulation theory based on multiparty sessiontypes where a choreography specification governs the behaviour of session typed processesand their observer. The bisimulation is defined with the observer cooperating withthe observed process in order to form complete global session scenarios and usable forproving correctness of optimisations for globally coordinating threads and processes. Theinduced bisimulation is strictly more fine-grained than the standard session bisimulation.The difference between the governed and standard bisimulations only appears when morethan two interleaved multiparty sessions exist. This distinct feature enables to reason realscenarios in the large-scale distributed system where multiple choreographic sessions needto be interleaved. The compositionality of the governed bisimilarity is proved through thesoundness and completeness with respect to the governed reduction-based congruence.Finally its usage is demonstrated by a thread transformation governed under multiple sessionsin a real usecase in the large-scale cyberinfrustracture.

Report

Denielou P-M, Yoshida N, 2013, Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types, AUTOMATA, LANGUAGES, AND PROGRAMMING, PT II, Vol: 7966, Pages: 174-186, ISSN: 0302-9743

Journal article

Coppo M, Dezani-Ciancaglini M, Padovani L, Yoshida Net al., 2013, Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions, COORDINATION MODELS AND LANGUAGES, COORDINATION 2013, Vol: 7890, Pages: 45-59, ISSN: 0302-9743

Journal article

Bocchi L, Chen T-C, Demangeon R, Honda K, Yoshida Net al., 2013, Monitoring Networks through Multiparty Session Types, FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, FMOODS/FORTE 2013, Vol: 7892, Pages: 50-65, ISSN: 0302-9743

Journal article

Bocchi L, Demangeon R, Yoshida N, 2013, A Multiparty Multi-session Logic, 7th International Symposium Trustworthy Global Computing (TGC), Publisher: SPRINGER-VERLAG BERLIN, Pages: 97-111, ISSN: 0302-9743

Conference paper

Ng N, Yoshida N, Luk W, 2013, Scalable Session Programming for Heterogeneous High-Performance Systems, Publisher: Springer, Pages: 82-98

Conference paper

Hu R, Neykova R, Yoshida N, Demangeon R, Honda Ket al., 2013, Practical Interruptible Conversations Distributed Dynamic Verification with Session Types and Python, 4th International Conference on Runtime Verification (RV), Publisher: SPRINGER-VERLAG BERLIN, Pages: 130-148, ISSN: 0302-9743

Conference paper

Neykova R, Yoshida N, Hu R, 2013, SPY: Local Verification of Global Protocols, 4th International Conference on Runtime Verification (RV), Publisher: SPRINGER-VERLAG BERLIN, Pages: 358-363, ISSN: 0302-9743

Conference paper

Henriksen AS, Nielsen L, Hildebrandt TT, Yoshida N, Henglein Fet al., 2013, Trustworthy Pervasive Healthcare Services via Multiparty Session Types, FOUNDATIONS OF HEALTH INFORMATION ENGINEERING AND SYSTEMS (FHIES 2012), Vol: 7789, Pages: 124-141, ISSN: 0302-9743

Journal article

Carbone M, Honda K, Yoshida N, 2012, Structured Communication-Centred Programming for Web Services, ACM TOPLAS

Journal article

Cortez C, Martins RM, Alves RM, Silva RC, Bilches LC, Macedo S, Atayde VD, Kawashita SY, Briones MRS, Yoshida Net al., 2012, Differential Infectivity by the Oral Route of <i>Trypanosoma cruzi</i> Lineages Derived from Y Strain, PLOS NEGLECTED TROPICAL DISEASES, Vol: 6, ISSN: 1935-2735

Journal article

Cortez C, Yoshida N, Bahia D, Sobreira TJPet al., 2012, Structural Basis of the Interaction of a <i>Trypanosoma cruzi</i> Surface Molecule Implicated in Oral Infection with Host Cells and Gastric Mucin, PLOS ONE, Vol: 7, ISSN: 1932-6203

Journal article

Chen TC, Bocchi L, Deniélou PM, Honda K, Yoshida Net al., 2012, Asynchronous distributed monitoring for multiparty session enforcement, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 7173 LNCS, Pages: 25-45, ISSN: 0302-9743

We propose a formal model of runtime safety enforcement for largescale, cross-language distributed applications with possibly untrusted endpoints. The underlying theory is based on multiparty session types with logical assertions (MPSA), an expressive protocol specification language that supports runtime validation through monitoring. Our method starts from global specifications based on MPSAs which the participants should obey. Distributed monitors use local specifications, projected from global specifications, to detect whether the interactions are well-behaved, and take appropriate actions, such as suppressing illegal messages. We illustrate the design of our model with examples from real-world distributed applications. We prove monitor transparency, communication conformance, and global session fidelity in the presence of possibly unsafe endpoints. © 2012 Springer-Verlag.

Journal article

Ng N, Yoshida N, Niu XY, Tsoi KH, Luk Wet al., 2012, Session types: towards safe and fast reconfigurable programming, ACM SIGARCH Computer Architecture News, Vol: 40, Pages: 22-22, ISSN: 0163-5964

This paper introduces a new programming framework based on the theory of session types for safe, recongurable parallel designs.We apply the session type theory to C and Java programming languages and demonstrate that the sessionbased languages can offer a clear and tractable framework to describe communications between parallel components and guarantee communication-safety and deadlock-freedom by compile-time type checking.Many representative communication topologies such as a ring or scatter-gather can be programmed and verified in session-based programming languages. Case studies involving N-body simulation and K-means clustering are used to illustrate the session-based programming style and to demonstrate that the session-based languages perform competitively against MPI counterparts in an FPGA-based heterogeneous cluster, as well as the potential of integrating them with FPGA acceleration.

Journal article

Maeda FY, Cortez C, Alves RM, Yoshida Net al., 2012, Mammalian cell invasion by closely related <i>Trypanosoma</i> species <i>T</i>. <i>dionisii</i> and <i>T</i>. <i>cruzi</i>, ACTA TROPICA, Vol: 121, Pages: 141-147, ISSN: 0001-706X

Journal article

Maeda FY, Cortez C, Yoshida N, 2012, Cell signaling during <i>Trypanosoma cruzi</i> invasion, FRONTIERS IN IMMUNOLOGY, Vol: 3, ISSN: 1664-3224

Journal article

Denielou P-M, Yoshida N, Bejleri A, Hu Ret al., 2012, PARAMETERISED MULTIPARTY SESSION TYPES, LOGICAL METHODS IN COMPUTER SCIENCE, Vol: 8, ISSN: 1860-5974

Journal article

Honda K, Marques ERB, Martins F, Ng N, Vasconcelos VT, Yoshida Net al., 2012, Verifications of MPI Programs using Session Types, EuroMPI’12, Pages: 291-293

Journal article

Fossati L, Honda K, Yoshida N, 2012, Intensional and Extensional Characterisation of Global Progress in the π-Calculus, CONCUR 2012 - CONCURRENCY THEORY, Vol: 7454, Pages: 287-301, ISSN: 0302-9743

Journal article

Crafa S, Varacca D, Yoshida N, 2012, Event Structure Semantics of Parallel Extrusion in the Pi-Calculus, FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, FOSSACS 2012, Vol: 7213, Pages: 225-239, ISSN: 0302-9743

Journal article

Denielou P-M, Yoshida N, 2012, Multiparty Session Types Meet Communicating Automata, 21st European Symposium on Programming (ESOP) held as Part of the 15th European Joint Conferences on Theory and Practice of Software (ETAPS), Publisher: SPRINGER-VERLAG BERLIN, Pages: 194-213, ISSN: 0302-9743

Conference paper

Ng N, Yoshida N, Honda K, 2012, Multiparty Session C: Safe Parallel Programming with Message Optimisation, Publisher: Springer, Pages: 202-218

Conference paper

Maeda FY, Alves RM, Cortez C, Lima FM, Yoshida Net al., 2011, Characterization of the infective properties of a new genetic group of <i>Trypanosoma cruzi</i> associated with bats, ACTA TROPICA, Vol: 120, Pages: 231-237, ISSN: 0001-706X

Journal article

Alves N, Hu R, Yoshida N, Deniélou P-Met al., 2011, Secure Execution of Distributed Session Programs, Electronic Proceedings in Theoretical Computer Science, Vol: 69, Pages: 1-11

Journal article

Yoshida N, Tyler KM, Llewellyn MS, 2011, Invasion mechanisms among emerging food-borne protozoan parasites, TRENDS IN PARASITOLOGY, Vol: 27, Pages: 459-466, ISSN: 1471-4922

Journal article

de Oliveira GM, Yoshida N, Higa EMS, Shenkman S, Alves M, Staquicini D, Cascabulho C, Schor Net al., 2011, Induction of proinflammatory cytokines and nitric oxide by Trypanosoma cruzi in renal cells, PARASITOLOGY RESEARCH, Vol: 109, Pages: 483-491, ISSN: 0932-0113

Journal article

Martins RM, Alves RM, Macedo S, Yoshida Net al., 2011, Starvation and rapamycin differentially regulate host cell lysosome exocytosis and invasion by <i>Trypanosoma cruzi</i> metacyclic forms, CELLULAR MICROBIOLOGY, Vol: 13, Pages: 943-954, ISSN: 1462-5814

Journal article

This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: limit=30&id=00365177&person=true&page=8&respub-action=search.html