Lost N Found

写在前面： 本文章是根据法国国立高等电力技术、电子学、计算机、水力学与电信学校 (E.N.S.E.E.I.H.T.) 第九学期课程 “Spécifications Formelles” 及以下参考资料总结而来的课程笔记。碍于本人学识有限，部分叙述难免存在纰漏，请读者注意甄别。 参考资料： Lost N Found 博客：Transition System(变迁系统) 与 TLA+ 知乎专栏：π-calculus 一、(Bi)Simulation 0 带标签的变迁系统 课程回顾：Transition System(变迁系统) 迹 (trace) 执行 (Exécutions) 相比于普通的变迁系统（三元组），带标签的变迁系统是一个四元组 ⟨S,L,I,R⟩\langle S, L, I, R \rangle⟨S,L,I,R⟩，其中： SSS 是这个系统的状态集。其可以是有限的，也可以是无限的。 LLL 是这个系统的字母表（alphabet），也即整个系统的标签集。 III 是这个系统的初始状态集，I⊆SI \subseteq SI⊆S。 RRR 用来描述这个系统各个状 ...

前言 本文为 MathJax/KaTex 在 Markdown 环境下的语法指引，内容完全参考自博客樱花赞：LaTeX公式手册(全网最全)。为了方便个人查找和添加规则，故拷贝至此。 参考文档： 樱花赞：LaTeX公式手册(全网最全) 维基百科的 数学公式教程； Cmd Markdown 公式指导手册。 如何插入公式 LaTeX\LaTeXLATE​X 的数学公式有两种：行中公式和独立公式（行间公式）。行中公式放在文中与其它文字混编，独立公式单独成行。 行中公式可以用如下方法表示：$ 数学公式 $，示例：行中数学公式行中数学公式行中数学公式 独立公式可以用如下方法表示：$$ 数学公式 $$，示例： 独立数学公式独立数学公式 独立数学公式 函数、符号及特殊字符 声调 / 变音符号 \dot{a}, \ddot{a}, \acute{a}, \grave{a} a˙,a¨,aˊ,aˋ{\displaystyle {\dot {a}},{\ddot {a}},{\acute {a}},{\grave { ...

信息安全的要素： 保密性（Confidentiality）：保证信息不被泄漏给未经授权的人，即使信息被截获，其表达的信息也不被非授权者所理解 →\to→ 加密。 完整性（Integrity）：防止信息被未经授权的人篡改。 可用性（Availability）：确保信息能被授权用户正常使用。 可控性 不可否认性：对出现的安全问题提供调查的依据和手段。查处恶意者。 对风险的应对：防御、检测、响应 在不考虑与互联网通信的完全封闭内部网时，我们需要考虑： 对于不同的工作人员分配不同的身份识别，应对其进行严格的访问控制；对于核心的重要敏感信息（企业内管理系统、数据库等）需要更加严格的身份识别、多因素身份验证。 对于不同的部门分配不同的子网划分，并在子网中继续划分 VLAN，这样可以控制访问、降低域内广播对于带宽的无效占用，以及缩小 ARP 类型攻击的受害范围； 在内网内也需要对于传送的信息进行加密，以防信息的泄漏； 对于所有部分（至少是重要的部分）都需要日志来记录所有用户的行为，为事后错误排查提供线索 如上图，在互联网边界可能存在如下安全风险： 来自互联网的 DoS 攻击（策略：A ...

写在前面： 本文章是根据法国国立高等电力技术、电子学、计算机、水力学与电信学校 (E.N.S.E.E.I.H.T.) 第九学期课程 “Formal development of complex system” 及以下参考资料总结而来的课程笔记。碍于本人学识有限，部分叙述难免存在纰漏，请读者注意甄别。 参考资料： 《Formal development of complex systems》Yamine AIT-AMEUR, Neeraj Kumar SINGH 《形式化方法：基于 B 方法的严格软件开发》裘宗燕，北京大学数学学院信息科学系 第一章：B 方法概述 第三章：集合论与逻辑 Oneree的博客：集合论与关系 零、前言 在软件工程的生命周期中，有一部分非常重要的工作，那就是进行需求分析和写出需求文档。 需求分析阶段需要清晰地说明什么是这个系统的功能和约束条件， 需求文档多半是使用自然语言写出的（大多数情况中，需求文档根本没有，或者写得很差）。需求文档如果不规范，会给后续阶段带来许多困难。特别是，由于需求文档的脆弱性，在设计阶段中就会出现不可避免的规范修改 ...

写在前面： 本文章是根据法国国立高等电力技术、电子学、计算机、水力学与电信学校 (E.N.S.E.E.I.H.T.) 第九学期课程 “Real Time System Scheduling” 及以下参考资料总结而来的课程笔记。碍于本人学识有限，部分叙述难免存在纰漏，请读者注意甄别。 一、什么是实时系统 1 实时系统的相关概念 与我们日常使用的操作系统不同，实时系统不仅要求计算结果正确，而且要求结果必须在一个特定的截止期限内产生（时间约束），否则即使正确也没有意义。 例如我们在实验中遇到的自平衡车：我们设计的系统需要根据传感器反馈的数据（加速度等）实时地调整车的姿态，从而使得车在一段时间内不会倾倒（时间约束），一旦超过这个时间，车就会倾倒，此时就算做出正确的调整也无济于事，因为车已经倒了。 “A real-time system is able, first to read all incoming data before they become useless, second to give an appropriate timely reaction.” “一个实时系统首先能够 ...

环境要求： JDK8 及以上 Maven 3.5 及以上 参考资料 SpringBoot 官网 SpringBoot 官方文档 SpringBoot 中文文档 哔哩哔哩：黑马程序员 SpringBoot 2 博客：未来很长，别只看眼前 学习的前置知识： 课程单元 前置知识 要求 基础篇 Java 基础语法 面向对象，封装，继承，多态，类与接口，集合，IO，网络编程等 基础篇 Spring 与 SpringMVC 知道 Spring 是用来管理 Bean，能够基于 RESTful 实现页面请求交互功能 基础篇 Mybatis 与 MybatisPlus 基于 Mybatis 和 MybatisPlus 能够开发出包含基础 CRUD 功能的标准 Dao 模块 基础篇 数据库 MySQL 能够读懂基础 CRUD 功能的 SQL 语句 基础篇 服务器 知道服务器与 web 工程的关系，熟悉web服务器的基础配置 基础篇 Maven 知道 Maven 的依赖关系，知道什么是依赖范围，依赖传递，排除依赖，可选依赖，继承 基础篇 WEB 技术（含vue， ...

写在前面： 本文章不会具体介绍 MPI 的历史发展，以及开发环境的过程配置，点击查看示例。 本文章将会使用 SimGrid 工具，来为异构分布式环境中的分布式应用程序仿真提供核心功能（模拟一个集群）。 建议使用 Docker 等容器化虚拟环境搭建测试开发平台，以下给出一个可用的 Docker 镜像文件。点击跳转至 DockerHub，或直接使用如下命令将镜像文件拉取到本地： 1docker pull henricasanova/ics632_smpi 我们使用 SimGrid 工具来模拟一个集群，集群的配置文件点击此处下载。为了后续运行方便，我们使用别名 alias 来简化 smpirun 指令的参数： 12345# init.sh# !/bin/bashSIMGRID=/集群配置文件的地址/alias smpirun="smpirun -hostfile ${SIMGRID}/archis/cluster_hostfile.txt -platform ${SIMGRID}/archis/cluster_crossbar ...

写在前面： 本文章是根据法国国立高等电力技术、电子学、计算机、水力学与电信学校 (E.N.S.E.E.I.H.T.) 第九学期课程 “Systèmes et algorithmes répartis” 及以下参考资料总结而来的课程笔记。碍于本人学识有限，部分叙述难免存在纰漏，请读者注意甄别。 参考资料： 《Systèmes et algorithmes répartis》Philippe Quéinnec, Gérard Padiou 《分布式计算——原理、算法与系统》 Kshemekalyani, A. D. and Singhal, M. 《分布式系统概念与设计》第5版 逻辑时钟-如何刻画分布式中的事件顺序 周刊（第22期）：图解一致性模型 - codedump’s blog YOUTUBE : CSE138 (Distributed Systems) lectures, Spring 2021 零、概述 我们把分布式系统定义成一个其硬件或软件组件分布在联网的计算机上，组件之间通过传递消息进行通信和动作协调的系统。这个简单的定义覆盖了所有可有效部署连网计算机的系统。由一个网 ...

写在前面： 本文章是根据法国国立高等电力技术、电子学、计算机、水力学与电信学校 (E.N.S.E.E.I.H.T.) 第九学期课程 “Web Semantic” 及以下参考资料总结而来的课程笔记。碍于本人学识有限，部分叙述难免存在纰漏，请读者注意甄别。 参考： 《知识工程及语义网技术》- 胡伟教授（南京大学） 课程视频资料：哔哩哔哩 - 个人主页：奋进的胡人Leo 教学课件 《语义网基础教程》- 第三版（机械工业出版社） 一、万维网与语义网，本体语言 0 引例 我们首先观察如下一个例子： 我们在搜索引擎搜索关键字 “Shiing-Shen Chern” 时，可以看到如下搜索结果。左边是传统的搜索结果，每一个结果都是一个页面；而在页面的右边，则是一个叫“知识卡片 (Knowledge Card)”的新特性。在知识卡片中给出了一些关于搜索结果的结构化的数据，如出生信息等。 从以上这个例子中我们看出，如今万维网搜索的新趋势不仅仅是寻找一个 Web 页面，而是寻求答案，理解概念并进行探索。在这种背景下，万维网该如何理解真实世界的事务，以及事物件的练习呢？ 谷歌提出了“知识 ...

一、SpringMVC 介绍 0 什么是 MVC 知识回顾：Appli Web课程笔记 - MVC 1 什么是 SpringMVC 在 Spring 中我们重点介绍了数据访问层 dao 与业务逻辑层 service 通过 Spring 框架的实现。SpringMVC 是 Spring 的一个子项目，是表述层 Controller 的一整套完备解决方案。 在如上的设计中： controller 负责请求和数据的接收，接收后将其转发给 service 进行业务处理 service 根据需要会调用 dao 对数据进行增删改查 dao 把数据处理完后，将结果交给 service，service再交给 controller controller 根据需求将 Model和 View 组合起来生成页面，转发给前端浏览器 这样做的好处就是 controller 可以处理多个请求，并对请求进行分发，执行不同的业务操作。 随着互联网的发展，上面的模式因为是同步调用，性能慢慢的跟不需求，所以异步调用 成为了如今流行的一种处理方式，如下图所示 因为是异步调用，所以后端不需要返回 View 视图 ...