การกำหนดคุณสมบัติโดยใช้แบบจำลองเป็นแนวทางหนึ่งในการกำหนดคุณสมบัติอย่างเป็นทางการโดยที่คุณสมบัติของระบบจะถูกแสดงออกมาในรูปของแบบจำลองสถานะของระบบแบบจำลองสถานะนี้สร้างขึ้นโดยใช้หน่วยทางคณิตศาสตร์ที่เข้าใจได้ง่าย เช่น เซตและฟังก์ชันการทำงานของระบบจะถูกกำหนดโดยการระบุว่ามันส่งผลต่อสถานะของแบบจำลองระบบอย่างไร

สัญกรณ์ที่ใช้กันอย่างแพร่หลายที่สุดสำหรับการพัฒนาข้อกำหนดตามแบบจำลองคือVDM ^{[ 1 ] [ 2 ]}และZ ^{[ 3 ] [ 4 ]} (ออกเสียงว่า เซด ไม่ใช่ ซี) สัญกรณ์เหล่านี้มีพื้นฐานมาจาก ทฤษฎีเซตแบบมีประเภทดังนั้น ระบบจึงถูกสร้างแบบจำลองโดยใช้เซตและความสัมพันธ์ระหว่างเซต

อีกหนึ่งแนวทางที่รู้จักกันดีในการกำหนดคุณสมบัติอย่างเป็นทางการคือการกำหนดคุณสมบัติเชิงพีชคณิต

• การออกแบบตามแบบจำลอง
• การทดสอบตามแบบจำลอง