Ran Wei/MDE 系列
English
基于 Eclipse Epsilon 的模型驱动工程 — Ran Wei

模型驱动工程与大语言模型

让大语言模型起草元模型和程序,用 Epsilon 检查草稿,并从模型生成提示词。

3 小时3 个时段8 个可运行示例Epsilon Playground

完成后你能够

  • 识别大语言模型草稿中需要形式检查之处。
  • 对示例性元模型与模型草稿运行 Epsilon 检查。
  • 从模型生成提示词而不调用在线大语言模型。

开始之前

建议先学习第 1 至 7 模块。除特别说明外,示例均可在 Playground 中运行。

下载本模块全部示例(zip)

目录

学习计划

3 小时

时间为估计值,包含运行示例的时间。进度保存在当前浏览器,中英文版本共享。

时段 160 分钟
起草并审查元模型
时段 260 分钟
检查模型草稿与断言
时段 360 分钟
应用与练习
1

把大语言模型用作起草助手

大语言模型可以建议元模型、示例模型或 Epsilon 程序。其回答只是草稿:文本可能能解析,却表达了错误的领域规则;看似合理的说明也可能与模型不符。用元模型定义结构,用 EVL 表达约束,再用可运行示例检验结果。大语言模型可以提出备选方案,最终应由模型中的证据判断方案是否成立。

本节改编自 Dimitris Kolovos 的 Metamodelling with ChatGPT, Episode 2。该实验发现,提供 Emfatic 示例有助于语言模型给出语法可用的草稿;后续反馈也改进了生成的 EGL 模板。下文的草稿是专为本教程编写的示例,不是该实验的原始输出,也不是实时生成的回答。示例不会调用大语言模型服务。

2

审查元模型草稿

第一个示例草稿把 Connector.source 和 Connector.target 都放宽为抽象的 Port 类型。因此,输入端口可以充当源,输出端口可以充当目标。EOL 查询成功运行,并打印出一条方向颠倒的连线。能解析、能运行只说明 Epsilon 能处理这些文件,并不证明连线规则正确。

示例示例草稿允许接反的连线在 Playground 中打开 ↗
inspect.eol
for (c in Connector.all) {
  (c.source.eContainer().name + "." + c.source.name + " -> " + c.target.eContainer().name + "." + c.target.name).println();
}
其他文件: alarm.flexmi, components.emf
alarm.flexmi
<?nsuri components?>
<architecture name="Alarm">
  <component name="OrGate">
    <inPort name="door" type="DIGITAL"/>
    <inPort name="window" type="DIGITAL"/>
    <outPort name="open" type="DIGITAL"/>
  </component>
  <component name="AndGate">
    <inPort name="open" type="DIGITAL"/>
    <inPort name="armed" type="DIGITAL"/>
    <outPort name="sound" type="DIGITAL"/>
  </component>
  <component name="Siren">
    <inPort name="sound" type="DIGITAL"/>
  </component>
  <connector source="Alarm.AndGate.open" target="Alarm.OrGate.open"/>
  <connector source="Alarm.AndGate.sound" target="Alarm.Siren.sound"/>
</architecture>
components.emf
@namespace(uri="components", prefix="components")
package components;

enum PortType {
  DIGITAL;
  ANALOG;
}

class Architecture {
  attr String[1] name;
  val Component[*]#architecture components;
  val Connector[*] connectors;
}

class Component {
  attr String[1] name;
  ref Architecture#components architecture;
  val Port[*] ports;
}

abstract class Port {
  attr String[1] name;
  attr PortType type;
}
class InPort extends Port {}
class OutPort extends Port {}

class Connector {
  ref Port source;
  ref Port target;
}
以下输出由构建本页时的 Epsilon 2.8.0 实际运行得到。Playground 中的提示措辞可能有所不同,并且不显示关于模型的警告。
输出
AndGate.open -> OrGate.open
AndGate.sound -> Siren.sound

可以要求起草助手列出类、包含关系、重数、端点方向,以及一个有效和一个无效的实例。逐项对照领域需求审查。尤其要检查 val 与 ref:连线引用组件拥有的端口,而不包含这些端口的副本。

3

检查模型草稿

EVL 可以把方向规则变成可执行的检查。下一项检查拒绝方向颠倒的连线,即使宽松的草稿元模型允许它。在 Playground 中,EVL 结果显示为模型图上的注释;下方记录了同一次验证运行的结果。

示例验证示例草稿在 Playground 中打开 ↗
rules.evl
context Connector {
  constraint OutputToInput {
    check: self.source.isTypeOf(OutPort) and self.target.isTypeOf(InPort)
    message: "Connector endpoints must run from OutPort to InPort"
  }
}
其他文件: alarm.flexmi, components.emf
alarm.flexmi
<?nsuri components?>
<architecture name="Alarm">
  <component name="OrGate">
    <inPort name="door" type="DIGITAL"/>
    <inPort name="window" type="DIGITAL"/>
    <outPort name="open" type="DIGITAL"/>
  </component>
  <component name="AndGate">
    <inPort name="open" type="DIGITAL"/>
    <inPort name="armed" type="DIGITAL"/>
    <outPort name="sound" type="DIGITAL"/>
  </component>
  <component name="Siren">
    <inPort name="sound" type="DIGITAL"/>
  </component>
  <connector source="Alarm.AndGate.open" target="Alarm.OrGate.open"/>
  <connector source="Alarm.AndGate.sound" target="Alarm.Siren.sound"/>
</architecture>
components.emf
@namespace(uri="components", prefix="components")
package components;

enum PortType {
  DIGITAL;
  ANALOG;
}

class Architecture {
  attr String[1] name;
  val Component[*]#architecture components;
  val Connector[*] connectors;
}

class Component {
  attr String[1] name;
  ref Architecture#components architecture;
  val Port[*] ports;
}

abstract class Port {
  attr String[1] name;
  attr PortType type;
}
class InPort extends Port {}
class OutPort extends Port {}

class Connector {
  ref Port source;
  ref Port target;
}
以下输出由构建本页时的 Epsilon 2.8.0 实际运行得到。Playground 中的提示措辞可能有所不同,并且不显示关于模型的警告。
输出
Error [OutputToInput]: Connector endpoints must run from OutPort to InPort

修正后的元模型限定源为 OutPort、目标为 InPort。修正后的模型也从 OrGate.open 指向 AndGate.open。同一 EVL 检查现在通过。

示例修正草稿并再次检查在 Playground 中打开 ↗
rules.evl
context Connector {
  constraint OutputToInput {
    check: self.source.isTypeOf(OutPort) and self.target.isTypeOf(InPort)
    message: "Connector endpoints must run from OutPort to InPort"
  }
}
其他文件: alarm.flexmi, components.emf
alarm.flexmi
<?nsuri components?>
<architecture name="Alarm">
  <component name="OrGate">
    <inPort name="door" type="DIGITAL"/>
    <inPort name="window" type="DIGITAL"/>
    <outPort name="open" type="DIGITAL"/>
  </component>
  <component name="AndGate">
    <inPort name="open" type="DIGITAL"/>
    <inPort name="armed" type="DIGITAL"/>
    <outPort name="sound" type="DIGITAL"/>
  </component>
  <component name="Siren">
    <inPort name="sound" type="DIGITAL"/>
  </component>
  <connector source="Alarm.OrGate.open" target="Alarm.AndGate.open"/>
  <connector source="Alarm.AndGate.sound" target="Alarm.Siren.sound"/>
</architecture>
components.emf
@namespace(uri="components", prefix="components")
package components;

enum PortType {
  DIGITAL;
  ANALOG;
}

class Architecture {
  attr String[1] name;
  val Component[*]#architecture components;
  val Connector[*] connectors;
}

class Component {
  attr String[1] name;
  ref Architecture#components architecture;
  val Port[*] ports;
}

abstract class Port {
  attr String[1] name;
  attr PortType type;
}
class InPort extends Port {}
class OutPort extends Port {}

class Connector {
  ref OutPort source;
  ref InPort target;
}
以下输出由构建本页时的 Epsilon 2.8.0 实际运行得到。Playground 中的提示措辞可能有所不同,并且不显示关于模型的警告。
输出
All constraints are satisfied.

两者提供不同的证据:元模型限制引用类型;EVL 则检查一条也适用于宽松草稿的规则。实际项目还应加入第 5 模块介绍的名称唯一性、信号类型兼容性和连线完整性检查。

4

验证生成的断言

起草助手可能声称警报模型有三条连线,实际只有两条。把这条示例性断言写成约束,差异便可观察,而不必依赖文字表述给人的可信感。

示例检验关于模型的草稿断言在 Playground 中打开 ↗
rules.evl
context Architecture {
  constraint ThreeConnectorsClaim {
    check: self.connectors.size() = 3
    message: "Draft claim said three connectors; model has " + self.connectors.size()
  }
}
其他文件: alarm.flexmi, components.emf
alarm.flexmi
<?nsuri components?>
<architecture name="Alarm">
  <component name="OrGate">
    <inPort name="door" type="DIGITAL"/>
    <inPort name="window" type="DIGITAL"/>
    <outPort name="open" type="DIGITAL"/>
  </component>
  <component name="AndGate">
    <inPort name="open" type="DIGITAL"/>
    <inPort name="armed" type="DIGITAL"/>
    <outPort name="sound" type="DIGITAL"/>
  </component>
  <component name="Siren">
    <inPort name="sound" type="DIGITAL"/>
  </component>
  <connector source="Alarm.OrGate.open" target="Alarm.AndGate.open"/>
  <connector source="Alarm.AndGate.sound" target="Alarm.Siren.sound"/>
</architecture>
components.emf
@namespace(uri="components", prefix="components")
package components;

enum PortType {
  DIGITAL;
  ANALOG;
}

class Architecture {
  attr String[1] name;
  val Component[*]#architecture components;
  val Connector[*] connectors;
}

class Component {
  attr String[1] name;
  ref Architecture#components architecture;
  val Port[*] ports;
}

abstract class Port {
  attr String[1] name;
  attr PortType type;
}
class InPort extends Port {}
class OutPort extends Port {}

class Connector {
  ref OutPort source;
  ref InPort target;
}
以下输出由构建本页时的 Epsilon 2.8.0 实际运行得到。Playground 中的提示措辞可能有所不同,并且不显示关于模型的警告。
输出
Error [ThreeConnectorsClaim]: Draft claim said three connectors; model has 2

将重要断言转换为测试或查询:元素数量、类型、可达性、唯一性及生成文件的内容。让断言与检查相邻。检查通过只支持它所检验的性质,并不证明整个设计正确。

5

从模型生成提示词

流程也可以从模型走向提示词。EGX 为每个组件创建一份审查提示词,EGL 填入实际端口名称。这些是供人或后续工具使用的文本文件;运行示例不会发送这些文件。

示例从组件生成审查提示词在 Playground 中打开 ↗
generate.egx
rule Component2Prompt
  transform c : Component {
  template: "template.egl"
  target: c.name + "-review.txt"
}
template.egl
[%
var prompt = "Review component " + c.name + ".\nInputs:";
for (p in c.ports.select(p | p.isTypeOf(InPort))) { prompt += " " + p.name; }
prompt += "\nOutputs:";
for (p in c.ports.select(p | p.isTypeOf(OutPort))) { prompt += " " + p.name; }
prompt += "\nCheck missing inputs and type mismatches against the model; do not invent ports.\n";
%][%=prompt%]
其他文件: alarm.flexmi, components.emf
alarm.flexmi
<?nsuri components?>
<architecture name="Alarm">
  <component name="OrGate">
    <inPort name="door" type="DIGITAL"/>
    <inPort name="window" type="DIGITAL"/>
    <outPort name="open" type="DIGITAL"/>
  </component>
  <component name="AndGate">
    <inPort name="open" type="DIGITAL"/>
    <inPort name="armed" type="DIGITAL"/>
    <outPort name="sound" type="DIGITAL"/>
  </component>
  <component name="Siren">
    <inPort name="sound" type="DIGITAL"/>
  </component>
  <connector source="Alarm.OrGate.open" target="Alarm.AndGate.open"/>
  <connector source="Alarm.AndGate.sound" target="Alarm.Siren.sound"/>
</architecture>
components.emf
@namespace(uri="components", prefix="components")
package components;

enum PortType {
  DIGITAL;
  ANALOG;
}

class Architecture {
  attr String[1] name;
  val Component[*]#architecture components;
  val Connector[*] connectors;
}

class Component {
  attr String[1] name;
  ref Architecture#components architecture;
  val Port[*] ports;
}

abstract class Port {
  attr String[1] name;
  attr PortType type;
}
class InPort extends Port {}
class OutPort extends Port {}

class Connector {
  ref OutPort source;
  ref InPort target;
}
以下输出由构建本页时的 Epsilon 2.8.0 实际运行得到。Playground 中的提示措辞可能有所不同,并且不显示关于模型的警告。
输出
--- AndGate-review.txt ---
Review component AndGate.
Inputs: open armed
Outputs: sound
Check missing inputs and type mismatches against the model; do not invent ports.
--- OrGate-review.txt ---
Review component OrGate.
Inputs: door window
Outputs: open
Check missing inputs and type mismatches against the model; do not invent ports.
--- Siren-review.txt ---
Review component Siren.
Inputs: sound
Outputs:
Check missing inputs and type mismatches against the model; do not invent ports.

提示词要求审查者不要编造端口,并对照源模型核查回答。如果之后使用大语言模型,应把回答另存为草稿,再运行相应的 Epsilon 检查。不要未经验证就把回答写入可信模型。

6

建立证据循环

从领域需求出发,撰写或请求一份草稿,运行解析器和检查,检查其输出,然后修订草稿。记录输入和准确的检查结果。对于生成的程序,至少在正常、边界和无效模型上运行;对于生成的文本,既要看生成器是否完成,也要检查生成文件。

不同工具检验不同问题:Emfatic 检验元模型语法,Flexmi 加载实例,EVL 检验领域约束,ETL 通过目标模型检验映射,EGL/EGX 展示生成文本。尚未形式化的需求仍须人工审查。

7

练习

练习 1★★★概念5 分钟

找出缺口。 为什么第一份草稿中首条连线方向颠倒,却仍能运行?

查看解答

两个端点引用都使用宽泛的 Port 类型,因此可以指向任一种具体端口。执行成功不代表满足预期的输出到输入规则。

练习 2★★★概念5 分钟

区分证据。 Emfatic 解析成功证明什么?EVL 方向约束又证明什么?

查看解答

解析成功表明元模型语法可处理。EVL 约束检查已加载模型中每条连线的方向。两者均不能单独证明全部领域需求。

练习 3★★★概念5 分钟

审查断言。 一段生成的文字声称有三个组件和三条连线。对于修正后的警报模型,哪一部分属实?

查看解答

模型确有 OrGate、AndGate、Siren 三个组件,但只有两条连线。应核对模型中的数量,而不是依赖文字。

练习 4★★★编程10 分钟

检查草稿方向。 添加 EVL 约束,拒绝源不是 OutPort 或目标不是 InPort 的连线。

查看解答

方向颠倒的示例草稿无法通过:

参考解答检查草稿中的端点方向在 Playground 中打开 ↗
rules.evl
context Connector {
  constraint Directed {
    check: self.source.isTypeOf(OutPort) and self.target.isTypeOf(InPort)
    message: "Reversed or incorrectly typed connector"
  }
}
其他文件: alarm.flexmi, components.emf
alarm.flexmi
<?nsuri components?>
<architecture name="Alarm">
  <component name="OrGate">
    <inPort name="door" type="DIGITAL"/>
    <inPort name="window" type="DIGITAL"/>
    <outPort name="open" type="DIGITAL"/>
  </component>
  <component name="AndGate">
    <inPort name="open" type="DIGITAL"/>
    <inPort name="armed" type="DIGITAL"/>
    <outPort name="sound" type="DIGITAL"/>
  </component>
  <component name="Siren">
    <inPort name="sound" type="DIGITAL"/>
  </component>
  <connector source="Alarm.AndGate.open" target="Alarm.OrGate.open"/>
  <connector source="Alarm.AndGate.sound" target="Alarm.Siren.sound"/>
</architecture>
components.emf
@namespace(uri="components", prefix="components")
package components;

enum PortType {
  DIGITAL;
  ANALOG;
}

class Architecture {
  attr String[1] name;
  val Component[*]#architecture components;
  val Connector[*] connectors;
}

class Component {
  attr String[1] name;
  ref Architecture#components architecture;
  val Port[*] ports;
}

abstract class Port {
  attr String[1] name;
  attr PortType type;
}
class InPort extends Port {}
class OutPort extends Port {}

class Connector {
  ref Port source;
  ref Port target;
}
以下输出由构建本页时的 Epsilon 2.8.0 实际运行得到。Playground 中的提示措辞可能有所不同,并且不显示关于模型的警告。
输出
Error [Directed]: Reversed or incorrectly typed connector
练习 5★★★编程10 分钟

核实数量。 用检查修正后警报模型恰有两条连线,取代错误的三条连线断言。

查看解答

修正后的模型通过检查:

参考解答验证两条连线的断言在 Playground 中打开 ↗
rules.evl
context Architecture {
  constraint TwoConnectors {
    check: self.connectors.size() = 2
    message: "Expected two connectors"
  }
}
其他文件: alarm.flexmi, components.emf
alarm.flexmi
<?nsuri components?>
<architecture name="Alarm">
  <component name="OrGate">
    <inPort name="door" type="DIGITAL"/>
    <inPort name="window" type="DIGITAL"/>
    <outPort name="open" type="DIGITAL"/>
  </component>
  <component name="AndGate">
    <inPort name="open" type="DIGITAL"/>
    <inPort name="armed" type="DIGITAL"/>
    <outPort name="sound" type="DIGITAL"/>
  </component>
  <component name="Siren">
    <inPort name="sound" type="DIGITAL"/>
  </component>
  <connector source="Alarm.OrGate.open" target="Alarm.AndGate.open"/>
  <connector source="Alarm.AndGate.sound" target="Alarm.Siren.sound"/>
</architecture>
components.emf
@namespace(uri="components", prefix="components")
package components;

enum PortType {
  DIGITAL;
  ANALOG;
}

class Architecture {
  attr String[1] name;
  val Component[*]#architecture components;
  val Connector[*] connectors;
}

class Component {
  attr String[1] name;
  ref Architecture#components architecture;
  val Port[*] ports;
}

abstract class Port {
  attr String[1] name;
  attr PortType type;
}
class InPort extends Port {}
class OutPort extends Port {}

class Connector {
  ref OutPort source;
  ref InPort target;
}
以下输出由构建本页时的 Epsilon 2.8.0 实际运行得到。Playground 中的提示措辞可能有所不同,并且不显示关于模型的警告。
输出
All constraints are satisfied.
练习 6★★★编程10 分钟

改进提示词。 在生成的审查提示词中加入每个端口的信号类型和具体端口类。

查看解答

模板遍历模型端口并输出其声明值:

参考解答生成包含类型的审查提示词在 Playground 中打开 ↗
generate.egx
rule Component2Prompt
  transform c : Component {
  template: "template.egl"
  target: c.name + "-typed-review.txt"
}
template.egl
Component [%=c.name%]
[% for (p in c.ports) { %][%=p.name%]: [%=p.type%] ([%=p.eClass().name%])
[% } %]Verify each connection against these declared ports. Report uncertainty explicitly.
其他文件: alarm.flexmi, components.emf
alarm.flexmi
<?nsuri components?>
<architecture name="Alarm">
  <component name="OrGate">
    <inPort name="door" type="DIGITAL"/>
    <inPort name="window" type="DIGITAL"/>
    <outPort name="open" type="DIGITAL"/>
  </component>
  <component name="AndGate">
    <inPort name="open" type="DIGITAL"/>
    <inPort name="armed" type="DIGITAL"/>
    <outPort name="sound" type="DIGITAL"/>
  </component>
  <component name="Siren">
    <inPort name="sound" type="DIGITAL"/>
  </component>
  <connector source="Alarm.OrGate.open" target="Alarm.AndGate.open"/>
  <connector source="Alarm.AndGate.sound" target="Alarm.Siren.sound"/>
</architecture>
components.emf
@namespace(uri="components", prefix="components")
package components;

enum PortType {
  DIGITAL;
  ANALOG;
}

class Architecture {
  attr String[1] name;
  val Component[*]#architecture components;
  val Connector[*] connectors;
}

class Component {
  attr String[1] name;
  ref Architecture#components architecture;
  val Port[*] ports;
}

abstract class Port {
  attr String[1] name;
  attr PortType type;
}
class InPort extends Port {}
class OutPort extends Port {}

class Connector {
  ref OutPort source;
  ref InPort target;
}
以下输出由构建本页时的 Epsilon 2.8.0 实际运行得到。Playground 中的提示措辞可能有所不同,并且不显示关于模型的警告。
输出
--- AndGate-typed-review.txt ---
Component AndGate
open: DIGITAL (InPort)
armed: DIGITAL (InPort)
sound: DIGITAL (OutPort)
Verify each connection against these declared ports. Report uncertainty explicitly.
--- OrGate-typed-review.txt ---
Component OrGate
door: DIGITAL (InPort)
window: DIGITAL (InPort)
open: DIGITAL (OutPort)
Verify each connection against these declared ports. Report uncertainty explicitly.
--- Siren-typed-review.txt ---
Component Siren
sound: DIGITAL (InPort)
Verify each connection against these declared ports. Report uncertainty explicitly.
8

自测

1
应怎样对待大语言模型建议的元模型?
2
宽泛的 Port 端点类型允许什么?
3
哪个示例将方向颠倒的连线判为违规?
4
修正后的警报模型有几条连线?
5
EGX 示例执行什么任务?
6
后续收到大语言模型回答后应该做什么?
7
一项约束通过能证明什么?
9

延伸阅读