More Web Proxy on the site http://driver.im/

research-article

Open access

Integration verification across software and hardware for a simple embedded system

Authors:

Samuel Gruetter,

Adam ChlipalaAuthors Info & Claims

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 604 - 619

https://doi.org/10.1145/3453483.3454065

Published: 18 June 2021 Publication History

Abstract

The interfaces between layers of a system are susceptible to bugs if developers of adjacent layers proceed under subtly different assumptions. Formal verification of two layers against the same formal model of the interface between them can be used to shake out these bugs. Doing so for every interface in the system can, in principle, yield unparalleled assurance of the correctness and security of the system as a whole. However, there have been remarkably few efforts that carry out this exercise, and all of them have simplified the task by restricting interactivity of the application, inventing new simplified instruction sets, and using unrealistic input and output mechanisms. We report on the first verification of a realistic embedded system, with its application software, device drivers, compiler, and RISC-V processor represented inside the Coq proof assistant as one mathematical object, with a machine-checked proof of functional correctness. A key challenge is structuring the proof modularly, so that further refinement of the components or expansion of the system can proceed without revisiting the rest of the system.

References

[1]

Eyad Alkassar, Mark A. Hillebrand, Steffen Knapp, Rostislav Rusev, and Sergey Tverdyshev. 2007. Formal Device and Programming Model for a Serial Interface. In Proceedings of 4th International Verification Workshop in Connection with CADE-21, Bremen, Germany, July 15-16, 2007, Bernhard Beckert (Ed.) (CEUR Workshop Proceedings, Vol. 259). CEUR-WS.org. http://ceur-ws.org/Vol-259/paper04.pdf

[2]

Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert W. Schirmer, and Artem Starostin. 2008. The Verisoft Approach to Systems Verification. In 2nd IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE’08), Natarajan Shankar and Jim Woodcock (Eds.) (LNCS, Vol. 5295). Springer, 209–224.

Digital Library

[3]

Andrew W. Appel. 2014. Program Logics - for Certified Compilers. Cambridge University Press. isbn:978-1-10-704801-0 https://www.cs.princeton.edu/~appel/papers/plcc.pdf

Digital Library

[4]

Krste Asanović, Rimas Avizienis, Jonathan Bachrach, Scott Beamer, David Biancolin, Christopher Celio, Henry Cook, Daniel Dabbelt, John Hauser, Adam Izraelevitz, Sagar Karandikar, Ben Keller, Donggyu Kim, John Koenig, Yunsup Lee, Eric Love, Martin Maas, Albert Magyar, Howard Mao, Miquel Moreto, Albert Ou, David A. Patterson, Brian Richards, Colin Schmidt, Stephen Twigg, Huy Vo, and Andrew Waterman. 2016. The Rocket Chip Generator. EECS Department, University of California, Berkeley. http://www2.eecs.berkeley.edu/Pubs/TechRpts/2016/EECS-2016-17.html

[5]

William R. Bevier, Warren A. Hunt, Jr., J. Strother Moore, and William D. Young. 1989. An approach to systems verification. J. Autom. Reasoning, 411–428. https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.68.6467&rep=rep1&type=pdf

[6]

Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay R. Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, and Jean Karim Zinzindohoue. 2017. Everest: Towards a Verified, Drop-in Replacement of HTTPS. In 2nd Summit on Advances in Programming Languages, SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA, Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi (Eds.) (LIPIcs, Vol. 71). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1:1–1:12. https://oadoi.org/10.4230/LIPIcs.SNAPL.2017.1

[7]

Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Andrew Wright, and Adam Chlipala. 2021. A Multipurpose Formal RISC-V Specification. arxiv:2104.00762.

[8]

Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, and Stephanie Weirich. 2018. Ready, Set, Verify! Applying Hs-to-Coq to Real-World Haskell Code (Experience Report). Proc. ACM Program. Lang., 2, ICFP (2018), Article 89, July, 16 pages. https://oadoi.org/10.1145/3236784

Digital Library

[9]

Hongxu Cai, Zhong Shao, and Alexander Vaynberg. 2007. Certified Self-Modifying Code. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’07). Association for Computing Machinery, New York, NY, USA. 66–77. isbn:9781595936332 https://oadoi.org/10.1145/1250734.1250743

Digital Library

[10]

Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, and Arvind. 2017. Kami: A Platform for High-level Parametric Hardware Specification and Its Modular Verification. Proc. ACM Program. Lang., 1, ICFP (2017), Article 24, Aug., 30 pages. issn:2475-1421 https://oadoi.org/10.1145/3110268

Digital Library

[11]

Ł ukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for Dependent Type Theory. Journal of Automated Reasoning, 61, 1-4 (2018), June, 423–453. issn:0168-7433, 1573-0670 https://oadoi.org/10.1007/s10817-018-9458-4

Digital Library

[12]

Matthias Daum, Norbert W. Schirmer, and Mareike Schmidt. 2010. From operating-system correctness to pervasively verified applications. In Proc. IFM. Springer-Verlag, 105–120. https://hal.inria.fr/inria-00524575/document

[13]

George Dunlap. 2012. The Intel SYSRET privilege escalation. https://xenproject.org/2012/06/13/the-intel-sysret-privilege-escalation/

[14]

Alex Dzyoba. 2014. A tale about data corruption, stack and red zone. https://alex.dzyoba.com/blog/redzone/

[15]

Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett. 2017. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In Computer Aided Verification, Rupak Majumdar and Viktor Kunčak (Eds.). 10427, Springer International Publishing, 126–133. isbn:978-3-319-63389-3 978-3-319-63390-9 https://homepage.divms.uiowa.edu/~tinelli/papers/EkiEtAl-CAV-17.pdf

[16]

M. Anton Ertl. 2015. What every compiler writer should know about programmers or “Optimization” based on undefined behaviour hurts performance. http://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_29.pdf

[17]

Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. 2017. Komodo: Using Verification to Disentangle Secure-Enclave Hardware from Software. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP ’17). Association for Computing Machinery, New York, NY, USA. 287–305. isbn:9781450350853 https://www.microsoft.com/en-us/research/wp-content/uploads/2017/10/komodo.pdf 10.1145/3132747.3132782.

Digital Library

[18]

Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). Association for Computing Machinery, Mumbai, India. 595–608. isbn:978-1-4503-3300-9 https://flint.cs.yale.edu/flint/publications/dscal.pdf 10.1145/2676726.2676975.

Digital Library

[19]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI’16). USENIX Association, USA. 653–669. isbn:9781931971331 https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu

Digital Library

[20]

Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). USENIX Association, Broomfield, CO. 165–181. isbn:978-1-931971-16-4 https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel

Digital Library

[21]

Warren A. Hunt. 1989. Microprocessor Design Verification. http://www.cs.utexas.edu/users/boyer/ftp/cli-reports/048.pdf

[22]

SiFive Inc. 2019. SiFive FE310-G000 Manual (v3p1). Available under “Freedom E310-G000” at https://www.sifive.com/documentation

[23]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. SeL4: Formal Verification of an OS Kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP ’09). Association for Computing Machinery, New York, NY, USA. 207–220. isbn:9781605587523 https://ts.data61.csiro.au/publications/nicta_full_text/3783.pdf 10.1145/1629575.1629596.

Digital Library

[24]

Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. 2019. From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019). Association for Computing Machinery, New York, NY, USA. 234–248. isbn:9781450362221 https://oadoi.org/10.1145/3293880.3294106

Digital Library

[25]

Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA. 179–191. isbn:9781450325448 https://ts.data61.csiro.au/publications/nicta_full_text/7494.pdf 10.1145/2535838.2535841.

Digital Library

[26]

Adam Langley. 2016. memcpy (and friends) with NULL pointers. https://www.imperialviolet.org/2016/06/26/nonnull.html

[27]

Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, 52, 7 (2009), 107–115. http://xavierleroy.org/publi/compcert-CACM.pdf

Digital Library

[28]

Xavier Leroy. 2009. A Formally Verified Compiler Back-End. Journal of Automated Reasoning, 43, 4 (2009), Dec., 363–446. issn:0168-7433, 1573-0670 https://oadoi.org/10.1007/s10817-009-9155-4

Digital Library

[29]

Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox. 2019. Verified compilation on a verified processor. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 1041–1053. https://cakeml.org/pldi19.pdf

Digital Library

[30]

William Mansky, Wolf Honoré, and Andrew W. Appel. 2020. Connecting Higher-Order Separation Logic to a First-Order Outside World. In Programming Languages and Systems, Peter Müller (Ed.). Springer International Publishing, Cham. 428–455. isbn:978-3-030-44914-8 https://oadoi.org/10.1007/978-3-030-44914-8_16

Digital Library

[31]

Kayvan Memarian and Peter Sewell. 2016. What is C in practice? (Cerberus survey v2): Analysis of Responses – with Comments. ISO SC22 WG14 N2015. http://www.cl.cam.ac.uk/~pes20/cerberus/analysis-2016-02-05-anon.txt

[32]

Magnus O. Myreen and Michael J. C. Gordon. 2007. Hoare logic for realistically modelled machine code. In In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), LNCS. Springer-Verlag, 568–582. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.96.2793

[33]

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP ’19). Association for Computing Machinery, New York, NY, USA. 225–242. isbn:9781450368735 https://oadoi.org/10.1145/3341301.3359641

Digital Library

[34]

Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP ’17). Association for Computing Machinery, New York, NY, USA. 252–269. isbn:9781450350853 https://oadoi.org/10.1145/3132747.3132748

Digital Library

[35]

C. H. Perleberg and A. J. Smith. 1993. Branch Target Buffer Design and Optimization. IEEE Trans. Comput., 42, 4 (1993), April, 396–412. issn:0018-9340 https://oadoi.org/10.1109/12.214687

Digital Library

[36]

Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. 2013. CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM, 60, 3 (2013), June, 1–50. issn:00045411 https://www.cl.cam.ac.uk/~pes20/CompCertTSO/doc/paper-long.pdf 10.1145/2487241.2487248.

Digital Library

[37]

David Shah, Eddie Hung, Clifford Wolf, Serge Bazanski, Dan Gisselquist, and Miodrag Milanović. 2019. Yosys+nextpnr: an Open Source Framework from Verilog to Bitstream for Commercial FPGAs. arxiv:1903.10407. 4 page short paper at IEEE FCCM 2019.

[38]

Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018. Nickel: A Framework for Design and Verification of Information Flow Control Systems. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI’18). USENIX Association, USA. 287–305. isbn:9781931971478 https://unsat.cs.washington.edu/papers/sigurbjarnarson-nickel.pdf

[39]

Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). Association for Computing Machinery, Mumbai, India. 275–287. isbn:978-1-4503-3300-9 https://www.cs.princeton.edu/~appel/papers/compcomp.pdf 10.1145/2676726.2676985.

[40]

Sergey Tverdyshev. 2009. Formal Verification of Gate-Level Computer Systems. Ph.D. Dissertation. Saarland University. http://www-wjp.cs.uni-saarland.de/publikationen/Tv09.pdf

[41]

Yuting Wang, Pierre Wilke, and Zhong Shao. 2019. An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code. Proc. ACM Program. Lang., 3, POPL (2019), Article 62, Jan., 30 pages. https://oadoi.org/10.1145/3290375

Digital Library

[42]

Andrew Waterman and Krste Asanovic. 2019. The RISC-V Instruction Set Manual. https://riscv.org/specifications/

[43]

Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, and George Candea. 2019. Verifying Software Network Functions with No Verification Expertise. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP ’19). Association for Computing Machinery, New York, NY, USA. 275–290. isbn:9781450368735 https://oadoi.org/10.1145/3341301.3359647

Digital Library

Cited By

Athalye ACorrigan-Gibbs HKaashoek FTassarotti JZeldovich NWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level ImplementationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695956(655-672)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695956
Erbsen APhilipoom JJamner DLin AGruetter SPit-Claudel CChlipala A(2024)Foundational Integration Verification of a Cryptographic ServerProceedings of the ACM on Programming Languages10.1145/36564468:PLDI(1704-1729)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656446
Gruetter SFukala VChlipala A(2024)Live Verification in an Interactive Proof AssistantProceedings of the ACM on Programming Languages10.1145/36564398:PLDI(1535-1558)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656439
Show More Cited By

Index Terms

Integration verification across software and hardware for a simple embedded system
1. Hardware
  1. Hardware validation
    1. Functional verification
      1. Theorem proving and SAT solving
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

Kami: a platform for high-level parametric hardware specification and its modular verification

It has become fairly standard in the programming-languages research world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that enables similar ...
HW/SW co-verification of embedded systems using bounded model checking
GLSVLSI '06: Proceedings of the 16th ACM Great Lakes symposium on VLSI

Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove the functional correctness. But in embedded system design the integration of software components becomes ...
Proof assistants at the hardware-software interface (invited talk)
CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

Some of the earliest applications of proof assistants were to correctness of digital hardware designs, but the subject doesn’t come up too frequently today at venues like CPP. I will try to make the case that proof assistants are a crucial tool for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2021

1341 pages

ISBN:9781450383912

DOI:10.1145/3453483

General Chair:
Stephen N. Freund
Williams College, USA
,
Program Chair:
Eran Yahav
Technion, Israel

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

PLDI '21

Sponsor:

SIGPLAN

PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 20 - 25, 2021

Virtual, Canada

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
1,378
Total Downloads

Downloads (Last 12 months)480
Downloads (Last 6 weeks)34

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Athalye ACorrigan-Gibbs HKaashoek FTassarotti JZeldovich NWitchel EArpaci-Dusseau ARossbach CKeeton K(2024)Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level ImplementationProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles10.1145/3694715.3695956(655-672)Online publication date: 4-Nov-2024
https://dl.acm.org/doi/10.1145/3694715.3695956
Erbsen APhilipoom JJamner DLin AGruetter SPit-Claudel CChlipala A(2024)Foundational Integration Verification of a Cryptographic ServerProceedings of the ACM on Programming Languages10.1145/36564468:PLDI(1704-1729)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656446
Gruetter SFukala VChlipala A(2024)Live Verification in an Interactive Proof AssistantProceedings of the ACM on Programming Languages10.1145/36564398:PLDI(1535-1558)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656439
Lorenzen ALeijen DSwierstra WLindley S(2024)The Functional Essence of Imperative Binary Search TreesProceedings of the ACM on Programming Languages10.1145/36563988:PLDI(518-542)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656398
Cohen JJohnson-Freyd P(2024)A Formalization of Core Why3 in CoqProceedings of the ACM on Programming Languages10.1145/36329028:POPL(1789-1818)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632902
Hammond ALiu ZPérami TSewell PBirkedal LPichon-Pharabod J(2024)An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL LogicProceedings of the ACM on Programming Languages10.1145/36328638:POPL(604-637)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632863
Busi MFocardi RLuccio F(2024)Bridging the Gap: Automated Analysis of Sancus2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00023(233-248)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00023
Athalye AKaashoek FZeldovich NTassarotti J(2023)The K2 Architecture for Trustworthy Hardware Security ModulesProceedings of the 1st Workshop on Kernel Isolation, Safety and Verification10.1145/3625275.3625402(26-32)Online publication date: 23-Oct-2023
https://dl.acm.org/doi/10.1145/3625275.3625402
Ho SFromherz AProtzenko J(2023)Modularity, Code Specialization, and Zero-Cost Abstractions for Program VerificationProceedings of the ACM on Programming Languages10.1145/36078447:ICFP(385-416)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607844
Bourgeat TClester IErbsen AGruetter SSingh PWright AChlipala A(2023)Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)Proceedings of the ACM on Programming Languages10.1145/36078337:ICFP(108-124)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607833
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents