Du bist nicht eingeloggt! Möglicherweise kannst du deswegen nicht alles sehen.
  (Noch kein mods.de-Account? / Passwort vergessen?)
Zur Übersichtsseite
Hallo anonymer User.
Bitte logge dich ein
oder registriere dich!
 Moderiert von: Irdorath, statixx, Teh Wizard of Aiz


 Thema: pOT-lnformatik, Mathematik, Physik XX ( Der XX(X)-Thread. )
« vorherige 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 [43] 44 45 46 47 48 49 50 nächste »
erste ungelesene Seite | letzter Beitrag 
Wraith of Seth

wraith_of_seth
 
Zitat von Wraith of Seth

Die Acta Physica Polonica (bzw. der Vorgänger der aktuellen Acta Physica Polonica B vor 1970) scheint nicht online zu sein.Hässlon
P.P.S. I can kill you with my brain.


...not fun fact: Die Acta Physica Polonica erschien nicht zwischen 1939 und 1947...traurig

Jehova! Jehova!
07.03.2017 15:02:22  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
dm-pandora

Gorge NaSe
Welch beschissenes Image in Verbindung mit nicht marktgerechter Entlohnung das Militär hat, weisst du ja sicherlich auch. Das Problem ist also diese Experten zu finden.
Und win2000 ist doch hypermodern, genauso wie serielle Schnittstellen - Maschinenbau und IT ein Drama in tausend Akten.
07.03.2017 15:03:56  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
SwissBushIndian

AUP SwissBushIndian 07.11.2011
Accenture bietet sowas zum Beispiel als Consultingservice an. Natürlich kostet das Geld, aber das ist mitunter einer der Gründe warum Militärprojekte meistens solche finanziellen Desaster sind. Davon sieht dann halt in der Regel der Contractor gar nichts. SAP ist auch auf Militärverträge spezialisiert, andere grössere Rüstungskolaborierer auch.
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von SwissBushIndian am 07.03.2017 15:09]
07.03.2017 15:08:00  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
dm-pandora

Gorge NaSe
 
Zitat von SwissBushIndian

Accenture bietet sowas zum Beispiel als Consultingservice an. Natürlich kostet das Geld, aber das ist mitunter einer der Gründe warum Militärprojekte meistens solche finanziellen Desaster sind. Davon sieht dann halt in der Regel der Contractor gar nichts. SAP ist auch auf Militärverträge spezialisiert, andere grössere Rüstungskolaborierer auch.



Die Idee mit Accenture finde ich gar nicht mal so schlecht, passt auch ganz gut in die aktuelle politische Linie. SAP wird gerade eh in die Bundeswehr eingeführt. Danke dir für deine Anregungen.
07.03.2017 15:13:48  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
wuSel

AUP wuSel 24.02.2008
 
Zitat von dm-pandora

 
Zitat von wuSel

 
Zitat von dm-pandora

Bei der Software um die es mir geht, wäre es schon besser wenn die fehlerfrei funktioniert peinlich/erstaunt.



Du bist Verkäufer oder Projektleiter oder?



Viel schlimmer ich soll den sicheren Betrieb von Waffenführungseinsatzsystemen in Verbindung mit zivilen und militärischen Navigationsequipment bescheinigen. Du denkst die freie Wirtschaft sei schlimm? Dann mache ich dich gerne mal mil. Zulieferern und Soldaten als Projektverantwortlichen bekannt.




Ich bin da bei SBI. Nach deiner Eingangsfrage bist du für die Bescheinigung wohl nicht so ganz der richtige oder? traurig

Und sicherer Betrieb ... da bist du nicht weit von meiner genannten Automatisierungstechniknorm weg. Da bescheinigen wir nämlich auch regelmäßig sicheren Betrieb von Anlagen. Dazu brauchst du aber eher sowas wie Aussagen des Konstrukteurs was überhaupt sicher zu machen ist. Augenzwinkern 100% perfekte Software gibt es auch da nicht. Dafür ist gerade die Safety ja da.
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von wuSel am 07.03.2017 16:03]
07.03.2017 16:01:14  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
dm-pandora

Gorge NaSe
 
Zitat von wuSel

 
Zitat von dm-pandora

 
Zitat von wuSel

 
Zitat von dm-pandora

Bei der Software um die es mir geht, wäre es schon besser wenn die fehlerfrei funktioniert peinlich/erstaunt.



Du bist Verkäufer oder Projektleiter oder?



Viel schlimmer ich soll den sicheren Betrieb von Waffenführungseinsatzsystemen in Verbindung mit zivilen und militärischen Navigationsequipment bescheinigen. Du denkst die freie Wirtschaft sei schlimm? Dann mache ich dich gerne mal mil. Zulieferern und Soldaten als Projektverantwortlichen bekannt.




Ich bin da bei SBI. Nach deiner Eingangsfrage bist du für die Bescheinigung wohl nicht so ganz der richtige oder? traurig

Und sicherer Betrieb ... da bist du nicht weit von meiner genannten Automatisierungstechniknorm weg. Da bescheinigen wir nämlich auch regelmäßig sicheren Betrieb von Anlagen. Dazu brauchst du aber eher sowas wie Aussagen des Konstrukteurs was überhaupt sicher zu machen ist. Augenzwinkern 100% perfekte Software gibt es auch da nicht. Dafür ist gerade die Safety ja da.



Vielleicht etwas missverständlich ausgedrückt, ich will die Software nicht selbst überprüfen und bescheinigen, sondern wissen welche Dokumente, Vorschriften und Verfahrensweisen üblicherweise genutzt werden um quasi einen sicheren Betrieb attestieren zu können.
07.03.2017 16:13:44  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
wuSel

AUP wuSel 24.02.2008
Klingt schon weniger wahnwitzig wenn ich dazu das Wort "Waffe" höre... Breites Grinsen
07.03.2017 16:16:44  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
krischan111

Arctic
Ich hatte mal mit einer Firma zu tun, die Steuergeräte für PKWs entwickelt hat. Einsatzzweck waren Serienfahrzeuge. Da kommen umfangreiche Hardware- und Softwarenormen ins Spiel. Der Entwicklungsprozess musste die Automotive Spice Richtlinie beachten. Jede einzelne Anforderung musste von der Erfassung bis zum Test der Implementierung getrackt werden. ISO 26262 (Funktionale Sicherheit für PKW) musste berücksichtigt werden und Risikoabschätzungen erstellt werden. Verschiedene Komponenten mussten ein Safety Integrity Level erreichen oder MISRA C/ MISRA C++ konform sein.

Die Implementierung an sich ist bei solchen Projekten der kleinste Teil. Augenzwinkern

Stand der Technik ist, dass man bei der professionellen Softwareentwicklung Best Practices beachtet (vor allem bei sicherheitsrelevanten Komponenten, wie SBI schrieb). Vor einiger Zeit gab es ja den Gerichtsprozess in Kalifornien, wo Toyota verurteilt wurde, weil ein PKW ungewollt beschleunigt hat. Dort wurde festgestellt, dass Toyota die Best Practices nicht hinreichend beachtet hatte.
07.03.2017 19:13:45  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
csde_rats

AUP csde_rats 04.09.2021
"dass Toyota die Best Practices nicht hinreichend beachtet hatte."

Das Protokoll der Zeugenaussage von Michael Barr ist öffentlich, und sehr gruselig. Der Zulieferer (Denso) hat da so richtigen Müll abgeliefert. Mit Highlights wie: Variablen-Mirroring, das nix tut. Watchdogs, die nix tun. 10000+ globale Variablen. Funktionen mit zyklomatischer Komplexität >9000 und und und.
07.03.2017 19:29:33  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
Skgoa

AUP Skgoa 10.11.2011
Das ist halt der Unterschied zwischen der deutschen und der nicht-deutschen Automobilindustrie. Augenzwinkern Ist ja nicht so, dass die Leute dum sind. Aber wenn der Kunde keine Anforderungen an die Qualität stellt, dann wirds halt Murks der gerade so funktioniert. Bei allen berechtigten Kritikpunkten sind die deutschen Hersteller da doch besser als die Billig-Konkurrenz.


 
Zitat von krischan111

Ich hatte mal mit einer Firma zu tun, die Steuergeräte für PKWs entwickelt hat. Einsatzzweck waren Serienfahrzeuge. Da kommen umfangreiche Hardware- und Softwarenormen ins Spiel. Der Entwicklungsprozess musste die Automotive Spice Richtlinie beachten. Jede einzelne Anforderung musste von der Erfassung bis zum Test der Implementierung getrackt werden. ISO 26262 (Funktionale Sicherheit für PKW) musste berücksichtigt werden und Risikoabschätzungen erstellt werden. Verschiedene Komponenten mussten ein Safety Integrity Level erreichen oder MISRA C/ MISRA C++ konform sein.


:X Deshalb: Prototypenprojekte > Serienprojekte


 
Zitat von krischan111
Die Implementierung an sich ist bei solchen Projekten der kleinste Teil. Augenzwinkern


komma her!
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von Skgoa am 07.03.2017 22:07]
07.03.2017 22:02:57  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
[smith]

AUP [smith] 29.07.2010
Vor vielen Jahren in meinem Studium hat ein Professor mal gesagt, dass medizinische Software durchaus mal z. B. per Hoare-Kalkül tatsächlich auf Korrektheit überprüft würde und es nicht total realitätsfern wäre, was wir da gerade lernen.
Hab ich nie wieder von gehört.

Davon abgesehen hoffe ich zumindest ein bisschen, dass es durchaus hohe Anforderungen z. B. für Software einer Beatmungsmaschine o. ä. gibt.

Im Energieversorgungsbereich kann ich euch allerdings auch jegliche Illusionen rauben. Wenn es da nicht immer noch ein paar wirklich schlaue Menschen gäbe, die am Ende die Schalter in der Hand haben, wäre es verdammt dunkel überall.

Und deshalb bin ich tatsächlich relativ froh, wenn ich derzeit Scheiße baue, können nur viele Leute keine Klamotten kaufen und die Firma verliert natürlich eine Menge Geld, aber nirgendwo geht das Licht dauerhaft aus oder fiese CERN-Laserroboter erheben sich peinlich/erstaunt
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von [smith] am 07.03.2017 22:38]
07.03.2017 22:36:44  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
SwissBushIndian

AUP SwissBushIndian 07.11.2011
Es gibt ja schon auch sowas wie Coq. Aber das kannst du halt höchstens für kleinste Subsysteme verwenden, das gleiche gilt wenn du das von Hand mit Hoare-Kalkül machst.

Und ganz ehrlich, von Medizinalsoftware habe ich leider bisher auch irgendwie nicht nur gutes gehört.

Die beste Closed Source Software die ich kenne ist ein Webserverplugin. Wenn der meiste Weltweit nur schon in der Qualität vorliegen würde, dann hätten wir definitiv weniger Probleme. Leider...
07.03.2017 22:40:21  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
derSenner

AUP derSenner 08.04.2020
Wenn du wüsstest, welche Software in sehr großen Krankenhäusern quasi den ganzen Betrieb aufrecht erhält, würdest du dir bei einem Schenkelbruch selbst das Bein zuhause amputieren. Gilt jetzt vor allen Dingen für Krankenhausinformationssysteme, die z.B. mit Picture Archiving Systems doch auch einiges verpfuschen können im Laufe deiner Diagnose.
Hat jetzt weniger was mit der Korrektheit eines Algorithmus zu tun, joa. Da geht's um superkomplexe Systeme, wo jeder Kackarzt glaubt reinpfuschen zu müssen. Ärzte sind sehr, sehr schwer mit Informationstechnologie zu vereinen.

// Editediteditedit
[Dieser Beitrag wurde 8 mal editiert; zum letzten Mal von derSenner am 07.03.2017 22:57]
07.03.2017 22:41:25  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
SwissBushIndian

AUP SwissBushIndian 07.11.2011
Breites Grinsen
07.03.2017 22:43:16  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
csde_rats

AUP csde_rats 04.09.2021
An der Stelle kann man mal nach "MUMPS (language)" googeln ...


Ironically, being inflicted with mumps (the disease) is much more pleasant that actually working with MUMPS (the language).
07.03.2017 23:24:14  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
SwissBushIndian

AUP SwissBushIndian 07.11.2011
Ich bin stets zur Stelle und poste das related:



¤: 19:30, irgendwie trollt mich der Timestamp mal wieder.
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von SwissBushIndian am 07.03.2017 23:27]
07.03.2017 23:25:43  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
derSenner

AUP derSenner 08.04.2020
 
Code:
set write="Hello world"
write write,!


07.03.2017 23:26:32  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
csde_rats

AUP csde_rats 04.09.2021
Appendix 7: An example of "traditional" M coding style

%DTC
%DTC ; SF/XAK - DATE/TIME OPERATIONS ;1/16/92  11:36 AM
     ;;19.0;VA FileMan;;Jul 14, 1992
     D    I 'X1!'X2 S X="" Q
     S X=X1 D H S X1=%H,X=X2,X2=%Y+1 D H S X=X1-%H,%Y=%Y+1&X2
     K %H,X1,X2 Q
     ;
C    S X=X1 Q:'X  D H S %H=%H+X2 D YMD S:$P(X1,".",2) X=X_"."_$P(X1,".",2) 
K X1,X2 Q
S    S %=%#60/100+(%#3600\60)/100+(%\3600)/100 Q
     ;
H    I X<1410000 S %H=0,%Y=-1 Q
     S %Y=$E(X,1,3),%M=$E(X,4,5),%D=$E(X,6,7)
     S %T=$E(X_0,9,10)*60+$E(X_"000",11,12)*60+$E(X_"00000",13,14)
TOH  S 
%H=%M>2&'(%Y#4)+$P("^31^59^90^120^151^181^212^243^273^304^334","^",%M)+%D
     S %='%M!'%D,%Y=%Y-141,%H=%H+(%Y*365)+(%Y\4)-(%Y>59)+%,%Y=$S(%:-
1,1:%H+4#7)
     K %M,%D,% Q
     ;
DOW  D H S Y=%Y K %H,%Y Q
DW   D H S Y=%Y,X=$P("SUN^MON^TUES^WEDNES^THURS^FRI^SATUR","^",Y+1)_"DAY"
     S:Y<0 X="" Q
7    S %=%H>21608+%H-.1,%Y=%\365.25+141,%=%#365.25\1
     S %D=%+306#(%Y#4=0+365)#153#61#31+1,%M=%-%D\29+1
     S X=%Y_"00"+%M_"00"+%D Q
     ;
YX   D YMD S Y=X_% G DD^%DT
YMD  D 7 S %=$P(%H,",",2) D S K %D,%M,%Y Q
T    F %=1:1 S Y=$E(X,%) Q:"+-"[Y  G 1^%DT:$E("TODAY",%)'=Y
     S X=$E(X,%+1,99) G PM:Y="" I +X'=X D DMW S X=%
     G:'X 1^%DT
PM   S @("%H=$H"_Y_X) D TT G 1^%DT:%I(3)'?3N,D^%DT
N    F %=2:1 S Y=$E(X,%) Q:"+-"[Y  G 1^%DT:$E("NOW",%)'=Y
     I Y="" S %H=$H G RT
     S X=$E(X,%+1,99)
     I X?1.N1"H" S X=X*3600,%H=$H,@("X=$P(%H,"","",2)"_Y_X),%=$S(X<0:-
1,1:0)+(X\86400),X=X#86400,%H=$P(%H,",")+%_","_X G RT
     D DMW G 1^%DT:'% S @("%H=$H"_Y_%),%H=%H_","_$P($H,",",2)
RT   D TT S %=$P(%H,",",2) D S S %=X_% I %DT'["S" S %=+$E(%,1,12)
     Q:'$D(%(0))  S Y=% G E^%DT
PF   S %H=$H D YMD S %(9)=X,X=%DT["F"*2-1 I @("%I(1)*100+%I(2)"_$E("> 
<",X+2)_"$E(%(9),4,7)") S %I(3)=%I(3)+X
     Q
TT   D 7 S %I(1)=%M,%I(2)=%D,%I(3)=%Y K %M,%D,%Y Q
NOW  S %H=$H,%H=$S($P(%H,",",2):%H,1:%H-1)
     D TT S %=$P(%H,",",2) D S S %=X_$S(%:%,1:.24) Q
DMW  S %=$S(X?1.N1"D":+X,X?1.N1"W":X*7,X?1.N1"M":X*30,+X=X:X,1:0)
     Q
COMMA     ;
     S %D=X<0 S:%D X=-X S %=$S($D(X2):+X2,1:2),X=$J(X,1,%),%=$L(X)-3-
$E(23456789,%),%L=$S($D(X3):X3,1:12)
     F %=%:-3 Q:$E(X,%)=""  S X=$E(X,1,%)_","_$E(X,%+1,99)
     S:$D(X2) X=$E("$",X2["$")_X S X=$J($E("(",%D)_X_$E(" )",%D+1),%L) K 
%,%D,%L
     Q
HELP S DDH=$S($D(DDH):DDH,1:0),A1="Examples of Valid Dates:" D %
     S A1="  JAN 20 1957 or 20 JAN 57 or 1/20/57"_$S(%DT'["N":" or 
012057",1:"") D %
     S A1="  T   (for TODAY),  T+1 (for TOMORROW),  T+2,  T+7,  etc." D %
     S A1="  T-1 (for YESTERDAY),  T-3W (for 3 WEEKS AGO), etc." D %
     S A1="If the year is omitted, the computer "_$S(%DT["P":"assumes a 
date in the PAST.",1:"uses the CURRENT YEAR.") D %
     I %DT'["X" S A1="You may omit the precise day, as:  JAN, 1957" D %
     I %DT'["T",%DT'["R" G 0
     S A1="If the date is omitted, the current date is assumed." D %
     S A1="Follow the date with a time, such as JAN 20@10, T@10AM, 10:30, 
etc." D %
     S A1="You may enter a time, such as NOON, MIDNIGHT or NOW." D %
     I %DT["S" S A1="Seconds may be entered as 10:30:30 or 103030AM." D %
     I %DT["R" S A1="Time is REQUIRED in this response." D %
0    Q:'$D(%DT(0))
     S A1=" " D % S A1="Enter a date which is "_$S(%DT(0)["-
":"less",1:"greater")_" than or equal to " D %
     S Y=$S(%DT(0)["-":$P(%DT(0),"-",2),1:%DT(0)) D DD^%DT:Y'["NOW"
     I '$D(DDS) W Y,"." K A1 Q
     S DDH(DDH,"T")=DDH(DDH,"T")_Y_"." K A1 Q
     ;
%    I '$D(DDS) W !,"     ",A1 Q
     S DDH=DDH+1,DDH(DDH,"T")="     "_A1 Q



e: Dann backlinken wir das einfach direkt: http://forum.mods.de/bb/thread.php?TID=215935&PID=1247026214#reply_1247026214
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von csde_rats am 07.03.2017 23:30]
07.03.2017 23:29:29  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
SwissBushIndian

AUP SwissBushIndian 07.11.2011
Ich habe Javacode gesehen der diesem Codestyle entsprechen muss. Ich würde das echt gerne zeigen weil es mir sonst niemand glaubt...
07.03.2017 23:31:18  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
statixx

AUP statixx 14.11.2023
verschmitzt lachen
Könnte auch ein Regex sein.
07.03.2017 23:32:04  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
derSenner

AUP derSenner 08.04.2020
Wisst ihr, irgendjemand muss sich da mal hingesetzt haben, und gesagt haben "Ja, das ist sehr, sehr gut so".

Wie?
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von derSenner am 07.03.2017 23:34]
07.03.2017 23:33:38  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
SwissBushIndian

AUP SwissBushIndian 07.11.2011
Vor allem muss man sich auf der Zunge zergehen lassen was es schon an guten Sprachen und Umgebungen gab. Irgendjemand hat also eigentlich einfach nur getrollt. Anders kann ich mir sowas wirklich nicht erklären. Oder wenn man halt wie Spongebob ist und unter einem Stein wohnt. Tief unter dem Meer...

¤: Das war der Seestern oder? Ja. So schlau sind die Leute wahrscheinlich auch.
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von SwissBushIndian am 07.03.2017 23:36]
07.03.2017 23:36:07  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
Danzelot

AUP Danzelot 28.02.2014
Ganz ehrlich, ich glaube niemand war je davon überzeugt dass so etwas eine gute Idee wäre. Wahrscheinlich hat einer da einen kleinen Mist gebaut, wollte aber nicht das Gesicht verlieren und einen Fehler eingestehen, und hat das deshalb gegenüber seinem Vorgesetzem mit Zähnen und Klauen verteidigt. Nach ein paar Iterationen hoch und runter durch die Managementebenen wurde dann von ganz oben entschieden dass das so eigentlich gut oder alternativ zu teuer zum Neumachen ist.
08.03.2017 0:15:35  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
wuSel

AUP wuSel 24.02.2008
 
Zitat von derSenner

Wenn du wüsstest, welche Software in sehr großen Krankenhäusern quasi den ganzen Betrieb aufrecht erhält, würdest du dir bei einem Schenkelbruch selbst das Bein zuhause amputieren. Gilt jetzt vor allen Dingen für Krankenhausinformationssysteme, die z.B. mit Picture Archiving Systems doch auch einiges verpfuschen können im Laufe deiner Diagnose.




Ich hab mich langsam über die letzten Jahre daran gewöhnt Kundschaft zu haben mit Anlagen wo der Verdienstausfall pro Stunde in netten 5stelligen Beträgen landet, die aber ihre Maschinen mit (Beispiel von Januar) IBM OS/2 betreiben "weil es ja noch geht". Der kriegt dann vielleicht doch mal eine Umrüstung dieses Jahr und die Hardware packen wir dann vorsichtig ein um sie nochmal jemandem als Ersatzteil verkaufen zu können. Breites Grinsen

DOS-Systeme in Firmen mit niemandem über 25 in der Instandhaltung ("Wie ich hab keine Maus?") fest verlötete Regelkreise ("Wie Sie können mir den Quellcode nicht einfach drucken?") und sowas sind dann noch das Sahnehäubchen.

Ich bin nur froh, dass eben keine Menschenleben von dem Kram abhängen.... nur regelmäßig Leute zu dumm zur Bedienung sind und sich hart verletzen oder umbringen. Die Ignoranz der Kundschaft bei Safety ist manchmal echt zum Haare ergrauen.
08.03.2017 11:20:04  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
B0rG*

Gordon
 
Zitat von SwissBushIndian

Es gibt ja schon auch sowas wie Coq. Aber das kannst du halt höchstens für kleinste Subsysteme verwenden, das gleiche gilt wenn du das von Hand mit Hoare-Kalkül machst.



Ich glaube nicht, dass es unmöglich ist, auch große Software zu verifizieren. CompCert ist ein mit Coq verifizierter C-Compiler, das würde ich ein größeres Stück Software nennen.

Das Problem ist glaube ich weniger die Theorie oder die prinzipielle Machbarkeit sondern mehr die Tatsache, dass die meisten Programmierer "da draußen" nicht wissen was sie tun und dementsprechende auch keinen verifizierten (oder auch nur prinzipiell verifizierbaren) Code schreiben können, denn der Code den sie schreiben ist inkorrekt. Da gibt's dann auch nichts zu beweisen.
08.03.2017 12:09:10  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
SwissBushIndian

AUP SwissBushIndian 07.11.2011
Ein Compiler ist aber vergleichsweise einfach. Ich habe eine Weile mit der Gruppe gearbeitet die probiert automatisches Testing für Eiffel zu implementieren. Eiffel als Sprache bringt schon viel mit (Design by Contract, Invarianten etc.) was einem dabei helfen sollte Testdaten zu generieren. Trotzdem ist es praktisch unmöglich ausser für die trivialsten Beispiele irgendwas funktionierendes zu machen.

Das Problem bei der ganzen Sache ist halt, dass Businesslogik nicht so schön zu analysieren ist wie zum Beispiel Parser/Lexer/Linker etc. Und so bald du Abhängigkeiten hast die nicht verifizierbar sind (Netzwerk, Strom, etc.) ist sowieso Hopfen und Malz verloren.

Ich bleibe dabei: wirklich komplexe Softwaresysteme zu verifizieren ist so gut wie unmöglich. Und natürlich kann man einzelne Teile davon verifizieren. Aber ob sich da der Aufwand lohnt ist dann halt wieder so eine Sache. Wenn du nicht komplett verifizieren kannst, dann kannst du dir wieder nicht sicher sein ob andere, nicht verifizierte Teile der Software zu Regressionen führen. Dann musst du deine Subsysteme alle strikt trennen und sicherstellen (haha), dass wie bei einem Monad nur saubere Daten in deine verifizierten Subsysteme geraten.

¤: Programmiergott sein hilft dann auch nur bedingt. Klar muss man einerseits in der Lage sein verifizierbaren Code zu schreiben. Das lässt sich mit Disziplin lernen. Aber es muss auch möglich sein ein verifizierbares System zu erstellen. Weitaus schwierigeres Problem.
[Dieser Beitrag wurde 2 mal editiert; zum letzten Mal von SwissBushIndian am 08.03.2017 13:14]
08.03.2017 13:08:01  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
csde_rats

AUP csde_rats 04.09.2021
Bei Compilern ist die Chance, dass es zumindest eine semi-formale Spezifikation für Teile gibt auch recht hoch (etwa für die Syntax).
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von csde_rats am 08.03.2017 13:20]
08.03.2017 13:18:03  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
B0rG*

Gordon
Ich stimme da bei allen Punkten zu. Ich würde aber dabei bleiben, dass das alles keine prinzipiellen Probleme sind, die es unmöglich machen, (formal) korrekte Software zu schreiben. Im Gegenteil: Eigentlich ist alles andere das Problem, was glaube ich auch genau der Punkt ist, den du machen willst. Mit dem Kommentar über Programmierer wollte ich meine Meinung zum Ausdruck bringen, dass "in der Praxis" selbst in der eingeschränkten Welt, in der es nur Software gibt, die formal spezifiziert werden kann, trotzdem die meiste Software scheisse wäre.

Davon unberührt steht die meiste Software nicht für sich allein sondern muss mit anderen Systemen interagieren. Wenn diese anderen Systeme kein verifizierbares Verhalten zeigen, wie du es nennst, dann kann man halt alle Beweise die man führt nur Bedingt auf irgendwelche Annahmen über diese Systeme führen. Das wäre aber auch besser als nichts und ist am Ende des Tages ja auch, was die ganzen Zertifizierungen versuchen, nur machen die das eben nicht formal. Ich gebe dir recht, dass das ein schwieriges Problem ist, aber ich bin da nicht so fundamental pessimistisch, dass das nicht funktionieren kann, wenn einen wirklich guten Grund hätte es zu tun. Leider qualifizieren Menschenleben offenbar nicht als "wirklich guter Grund" (siehe Toyota), sehr teure Experimente im Weltall aber schon eher (siehe NASA).
[Dieser Beitrag wurde 1 mal editiert; zum letzten Mal von B0rG* am 08.03.2017 13:42]
08.03.2017 13:40:05  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
SwissBushIndian

AUP SwissBushIndian 07.11.2011
Ich würde so weit gehen zu behaupten, dass alles andere komplett überwiegt. Aber ja, wir sind uns komplett einig. Und wenn man völlig realistisch ist wird es überhaupt erst so weit kommen wenn das Tooling vollautomatisch ist. Wenn man nur schon schaut wie viel zu wenig Software getestet wird (was ziemliches Mainstream wissen ist) kann man davon gut ableiten wie gross das Interesse ist verifizierte Software zu schreiben. Kostet halt auch Geld und Zeit.
08.03.2017 13:46:33  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
Wraith of Seth

wraith_of_seth
unglaeubig gucken
TIL: Zyklische Vertauschungen beim Levi-Civita in 4D sind nicht alle gerade.

...wie in drei Teufels Namen habe ich eigentlich meinen Abschluss bekommen?

Kopf gegen die Wand schlagen

Diese Erkenntnis vor zwei Wochen hätte mir zwei Wochen gespart. Wieso ich da noch nicht vorher drüber gestolpert bin (z.B. bei diversen(!) Klausuren...) ist mir schleierhaft.

Amen. Halleluja. Erdnussbutter.
09.03.2017 12:32:17  Zum letzten Beitrag
[ zitieren ] [ pm ] [ diesen post melden ]
 Thema: pOT-lnformatik, Mathematik, Physik XX ( Der XX(X)-Thread. )
« vorherige 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 [43] 44 45 46 47 48 49 50 nächste »

mods.de - Forum » Public Offtopic » 

Hop to:  

Mod-Aktionen:
30.04.2017 22:10:02 Sharku hat diesen Thread geschlossen.
11.05.2016 21:00:25 Sharku hat diesem Thread das ModTag 'pimp' angehängt.

| tech | impressum