Difference between revisions of "Applications"
From The Maude System
Line 13: | Line 13: | ||
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://dblp.org/rec/conf/indocrypt/Aparicio-Sanchez20.bib AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]). | * Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://dblp.org/rec/conf/indocrypt/Aparicio-Sanchez20.bib AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]). | ||
− | * Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ | + | * Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]) |
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). | * Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). | ||
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features. | * Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features. |
Revision as of 21:40, 20 December 2020
Maude and its formal tools have been used in many pioneering applications:
- Formal definition and verification of programming and hardware, resp. software, modeling languages: full C (ER12), Java (FCMR04), JVM (FMR04), NASA’s PLEXIL (RCMS12), Verilog (MKMR10), E-LOTOS (V02, VM05), UML (CE06, DRMA14), MOF (BM10), ODP (DV03, DRV05, RVD07), AADL (BOM14), Ptolemy (BOFLT14), and BPMN (DS17, DRS18).
- Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer (CMSWW07), and design and verification of the secure-by-construction Illinois’s IBOS browser (SKMT12, SMR20).
- Cryptographic protocol analysis: Maude-NPA has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM (GAEMM18), IBM’s CCA (GSEMM14), and PCKS#11 (GSEMM15), using unification and symbolic reachability. Tamarin, resp. AKISS, use Maude’s unification to analyze protocols like 5G-AKA (DC18), resp. RFID (GK17).
- Network protocols: AER/NCA active networks (OKMTZ06), MANETS (LOM16), BGP (Wetal13, Wetal11, WTGLS12); DDoS-Intruder models; and DDoS protection (LDFN18): ASV (AMG09), Stable Availability (EMMW12), VoIP-SIP (SASGM09), using Maude’s statistical model checking (SMC) tool.
- Cloud transaction system formalization and analysis: Cassandra (LNGRG15), Google’s Megastore (GO14), P-Store (O17), etc. (Betal18), using SMC.
- Analysis of real-time and cyber-physical systems: CASH scheduling (OC06), sensor (OT09) and MANET (LOM16) networks, timed security protocols (AEMMS20), PALS transformation from synchronous to correct distributed real-time systems (MO12, BMO12) enables model checking of complex models such as AADL and Ptolemy models (BOM14) and distributed control of airplane maneuvers (BKMO12).
- Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. (Pathway Logic)
- Specification and analysis of models of Concurrency: Petri Nets (SMO01), CCS, pi-Calculus ([1]), Actors (M93), REO (MSA), Orc (AM15).
- Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube (SM04), linear logic (MM02), modal logics (OPR18), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive (DM12, DMR20) and Reachability Logic (SSM17), theorem provers, HOL-to-Nuprl translator (NSM01), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.